Theorem eqrelrd2

Description: A version of eqrelrdv2 with explicit nonfree declarations. (Contributed by Thierry Arnoux, 28-Aug-2017)

	Ref	Expression
Hypotheses	eqrelrd2.1	⊢ Ⅎ 𝑥 𝜑
	eqrelrd2.2	⊢ Ⅎ 𝑦 𝜑
	eqrelrd2.3	⊢ Ⅎ 𝑥 𝐴
	eqrelrd2.4	⊢ Ⅎ 𝑦 𝐴
	eqrelrd2.5	⊢ Ⅎ 𝑥 𝐵
	eqrelrd2.6	⊢ Ⅎ 𝑦 𝐵
	eqrelrd2.7	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
Assertion	eqrelrd2	⊢ ( ( ( Rel 𝐴 ∧ Rel 𝐵 ) ∧ 𝜑 ) → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqrelrd2.1	⊢ Ⅎ 𝑥 𝜑
2		eqrelrd2.2	⊢ Ⅎ 𝑦 𝜑
3		eqrelrd2.3	⊢ Ⅎ 𝑥 𝐴
4		eqrelrd2.4	⊢ Ⅎ 𝑦 𝐴
5		eqrelrd2.5	⊢ Ⅎ 𝑥 𝐵
6		eqrelrd2.6	⊢ Ⅎ 𝑦 𝐵
7		eqrelrd2.7	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
8	2 7	alrimi	⊢ ( 𝜑 → ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
9	1 8	alrimi	⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
10	9	adantl	⊢ ( ( ( Rel 𝐴 ∧ Rel 𝐵 ) ∧ 𝜑 ) → ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
11	1 2 3 4 5 6	ssrelf	⊢ ( Rel 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
12	1 2 5 6 3 4	ssrelf	⊢ ( Rel 𝐵 → ( 𝐵 ⊆ 𝐴 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
13	11 12	bi2anan9	⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) ) )
14		eqss	⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
15		2albiim	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ∧ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
16	13 14 15	3bitr4g	⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
17	16	adantr	⊢ ( ( ( Rel 𝐴 ∧ Rel 𝐵 ) ∧ 𝜑 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
18	10 17	mpbird	⊢ ( ( ( Rel 𝐴 ∧ Rel 𝐵 ) ∧ 𝜑 ) → 𝐴 = 𝐵 )