Metamath Proof Explorer


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 𝐵 ) ∧ 𝜑 ) → 𝐴 = 𝐵 )