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 ⊢ Ⅎ x φ
eqrelrd2.2 ⊢ Ⅎ y φ
eqrelrd2.3 ⊢ Ⅎ _ x A
eqrelrd2.4 ⊢ Ⅎ _ y A
eqrelrd2.5 ⊢ Ⅎ _ x B
eqrelrd2.6 ⊢ Ⅎ _ y B
eqrelrd2.7 ⊢ φ → x y ∈ A ↔ x y ∈ B
Assertion eqrelrd2 ⊢ Rel ⁡ A ∧ Rel ⁡ B ∧ φ → A = B

Proof

Step Hyp Ref Expression
1 eqrelrd2.1 ⊢ Ⅎ x φ
2 eqrelrd2.2 ⊢ Ⅎ y φ
3 eqrelrd2.3 ⊢ Ⅎ _ x A
4 eqrelrd2.4 ⊢ Ⅎ _ y A
5 eqrelrd2.5 ⊢ Ⅎ _ x B
6 eqrelrd2.6 ⊢ Ⅎ _ y B
7 eqrelrd2.7 ⊢ φ → x y ∈ A ↔ x y ∈ B
8 2 7 alrimi ⊢ φ → ∀ y x y ∈ A ↔ x y ∈ B
9 1 8 alrimi ⊢ φ → ∀ x ∀ y x y ∈ A ↔ x y ∈ B
10 9 adantl ⊢ Rel ⁡ A ∧ Rel ⁡ B ∧ φ → ∀ x ∀ y x y ∈ A ↔ x y ∈ B
11 1 2 3 4 5 6 ssrelf ⊢ Rel ⁡ A → A ⊆ B ↔ ∀ x ∀ y x y ∈ A → x y ∈ B
12 1 2 5 6 3 4 ssrelf ⊢ Rel ⁡ B → B ⊆ A ↔ ∀ x ∀ y x y ∈ B → x y ∈ A
13 11 12 bi2anan9 ⊢ Rel ⁡ A ∧ Rel ⁡ B → A ⊆ B ∧ B ⊆ A ↔ ∀ x ∀ y x y ∈ A → x y ∈ B ∧ ∀ x ∀ y x y ∈ B → x y ∈ A
14 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
15 2albiim ⊢ ∀ x ∀ y x y ∈ A ↔ x y ∈ B ↔ ∀ x ∀ y x y ∈ A → x y ∈ B ∧ ∀ x ∀ y x y ∈ B → x y ∈ A
16 13 14 15 3bitr4g ⊢ Rel ⁡ A ∧ Rel ⁡ B → A = B ↔ ∀ x ∀ y x y ∈ A ↔ x y ∈ B
17 16 adantr ⊢ Rel ⁡ A ∧ Rel ⁡ B ∧ φ → A = B ↔ ∀ x ∀ y x y ∈ A ↔ x y ∈ B
18 10 17 mpbird ⊢ Rel ⁡ A ∧ Rel ⁡ B ∧ φ → A = B