Theorem eqrelf

Description: The equality connective between relations. (Contributed by Peter Mazsa, 25-Jun-2019)

	Ref	Expression
Hypotheses	eqrelf.1	⊢ Ⅎ 𝑥 𝐴
	eqrelf.2	⊢ Ⅎ 𝑥 𝐵
	eqrelf.3	⊢ Ⅎ 𝑦 𝐴
	eqrelf.4	⊢ Ⅎ 𝑦 𝐵
Assertion	eqrelf	⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqrelf.1	⊢ Ⅎ 𝑥 𝐴
2		eqrelf.2	⊢ Ⅎ 𝑥 𝐵
3		eqrelf.3	⊢ Ⅎ 𝑦 𝐴
4		eqrelf.4	⊢ Ⅎ 𝑦 𝐵
5		eqrel	⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑢 ∀ 𝑣 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ) ) )
6		nfv	⊢ Ⅎ 𝑢 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
7		nfv	⊢ Ⅎ 𝑣 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
8	1	nfel2	⊢ Ⅎ 𝑥 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴
9	2	nfel2	⊢ Ⅎ 𝑥 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵
10	8 9	nfbi	⊢ Ⅎ 𝑥 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
11	3	nfel2	⊢ Ⅎ 𝑦 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴
12	4	nfel2	⊢ Ⅎ 𝑦 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵
13	11 12	nfbi	⊢ Ⅎ 𝑦 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 )
14		opeq12	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ )
15	14	eleq1d	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴 ) )
16	14	eleq1d	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ) )
17	15 16	bibi12d	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ) ) )
18	6 7 10 13 17	cbval2v	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ∀ 𝑢 ∀ 𝑣 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐴 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝐵 ) )
19	5 18	bitr4di	⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )