This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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