Axiom ax-L8-inr 21

Description: Right '∈' substitution.

Assertion

Ref	Expression
ax-L8-inr	⊢ (𝑡 = 𝑢 → (𝑤 ∈ 𝑡 → 𝑤 ∈ 𝑢))

Detailed syntax breakdown of Axiom ax-L8-inr

Step	Hyp	Ref	Expression
1		term-t	. . 3 term 𝑡
2		term-u	. . 3 term 𝑢
3	1, 2	wff-equals 6	. 2 wff 𝑡 = 𝑢
4		term-w	. . . 4 term 𝑤
5	4, 1	wff-elemof 7	. . 3 wff 𝑤 ∈ 𝑡
6	4, 2	wff-elemof 7	. . 3 wff 𝑤 ∈ 𝑢
7	5, 6	wff-imp 10	. 2 wff (𝑤 ∈ 𝑡 → 𝑤 ∈ 𝑢)
8	3, 7	wff-imp 10	1 wff (𝑡 = 𝑢 → (𝑤 ∈ 𝑡 → 𝑤 ∈ 𝑢))

This axiom is referenced by:  subelofr-P5  640