Theorem eqer

Description: Equivalence relation involving equality of dependent classes A ( x ) and B ( y ) . (Contributed by NM, 17-Mar-2008) (Revised by Mario Carneiro, 12-Aug-2015) (Proof shortened by AV, 1-May-2021)

	Ref	Expression
Hypotheses	eqer.1	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
	eqer.2	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝐴 = 𝐵 }
Assertion	eqer	⊢ 𝑅 Er V

Proof

Step	Hyp	Ref	Expression
1		eqer.1	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
2		eqer.2	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝐴 = 𝐵 }
3	2	relopabiv	⊢ Rel 𝑅
4		id	⊢ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 )
5	4	eqcomd	⊢ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 → ⦋ 𝑤 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
6	1 2	eqerlem	⊢ ( 𝑧 𝑅 𝑤 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 )
7	1 2	eqerlem	⊢ ( 𝑤 𝑅 𝑧 ↔ ⦋ 𝑤 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
8	5 6 7	3imtr4i	⊢ ( 𝑧 𝑅 𝑤 → 𝑤 𝑅 𝑧 )
9		eqtr	⊢ ( ( ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 ∧ ⦋ 𝑤 / 𝑥 ⦌ 𝐴 = ⦋ 𝑣 / 𝑥 ⦌ 𝐴 ) → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑣 / 𝑥 ⦌ 𝐴 )
10	1 2	eqerlem	⊢ ( 𝑤 𝑅 𝑣 ↔ ⦋ 𝑤 / 𝑥 ⦌ 𝐴 = ⦋ 𝑣 / 𝑥 ⦌ 𝐴 )
11	6 10	anbi12i	⊢ ( ( 𝑧 𝑅 𝑤 ∧ 𝑤 𝑅 𝑣 ) ↔ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑤 / 𝑥 ⦌ 𝐴 ∧ ⦋ 𝑤 / 𝑥 ⦌ 𝐴 = ⦋ 𝑣 / 𝑥 ⦌ 𝐴 ) )
12	1 2	eqerlem	⊢ ( 𝑧 𝑅 𝑣 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑣 / 𝑥 ⦌ 𝐴 )
13	9 11 12	3imtr4i	⊢ ( ( 𝑧 𝑅 𝑤 ∧ 𝑤 𝑅 𝑣 ) → 𝑧 𝑅 𝑣 )
14		vex	⊢ 𝑧 ∈ V
15		eqid	⊢ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴
16	1 2	eqerlem	⊢ ( 𝑧 𝑅 𝑧 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
17	15 16	mpbir	⊢ 𝑧 𝑅 𝑧
18	14 17	2th	⊢ ( 𝑧 ∈ V ↔ 𝑧 𝑅 𝑧 )
19	3 8 13 18	iseri	⊢ 𝑅 Er V