Metamath Proof Explorer

Theorem mpo2eqb

Description: Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 . (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Assertion mpo2eqb ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → x ∈ A , y ∈ B ⟼ C = x ∈ A , y ∈ B ⟼ D ↔ ∀ x ∈ A ∀ y ∈ B C = D

Proof

Step Hyp Ref Expression
1 df-mpo ⊢ x ∈ A , y ∈ B ⟼ C = x y z | x ∈ A ∧ y ∈ B ∧ z = C
2 df-mpo ⊢ x ∈ A , y ∈ B ⟼ D = x y z | x ∈ A ∧ y ∈ B ∧ z = D
3 1 2 eqeq12i ⊢ x ∈ A , y ∈ B ⟼ C = x ∈ A , y ∈ B ⟼ D ↔ x y z | x ∈ A ∧ y ∈ B ∧ z = C = x y z | x ∈ A ∧ y ∈ B ∧ z = D
4 eqoprab2bw ⊢ x y z | x ∈ A ∧ y ∈ B ∧ z = C = x y z | x ∈ A ∧ y ∈ B ∧ z = D ↔ ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z = C ↔ x ∈ A ∧ y ∈ B ∧ z = D
5 pm5.32 ⊢ x ∈ A ∧ y ∈ B → z = C ↔ z = D ↔ x ∈ A ∧ y ∈ B ∧ z = C ↔ x ∈ A ∧ y ∈ B ∧ z = D
6 5 albii ⊢ ∀ z x ∈ A ∧ y ∈ B → z = C ↔ z = D ↔ ∀ z x ∈ A ∧ y ∈ B ∧ z = C ↔ x ∈ A ∧ y ∈ B ∧ z = D
7 19.21v ⊢ ∀ z x ∈ A ∧ y ∈ B → z = C ↔ z = D ↔ x ∈ A ∧ y ∈ B → ∀ z z = C ↔ z = D
8 6 7 bitr3i ⊢ ∀ z x ∈ A ∧ y ∈ B ∧ z = C ↔ x ∈ A ∧ y ∈ B ∧ z = D ↔ x ∈ A ∧ y ∈ B → ∀ z z = C ↔ z = D
9 8 2albii ⊢ ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z = C ↔ x ∈ A ∧ y ∈ B ∧ z = D ↔ ∀ x ∀ y x ∈ A ∧ y ∈ B → ∀ z z = C ↔ z = D
10 r2al ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z z = C ↔ z = D ↔ ∀ x ∀ y x ∈ A ∧ y ∈ B → ∀ z z = C ↔ z = D
11 9 10 bitr4i ⊢ ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z = C ↔ x ∈ A ∧ y ∈ B ∧ z = D ↔ ∀ x ∈ A ∀ y ∈ B ∀ z z = C ↔ z = D
12 3 4 11 3bitri ⊢ x ∈ A , y ∈ B ⟼ C = x ∈ A , y ∈ B ⟼ D ↔ ∀ x ∈ A ∀ y ∈ B ∀ z z = C ↔ z = D
13 pm13.183 ⊢ C ∈ V → C = D ↔ ∀ z z = C ↔ z = D
14 13 ralimi ⊢ ∀ y ∈ B C ∈ V → ∀ y ∈ B C = D ↔ ∀ z z = C ↔ z = D
15 ralbi ⊢ ∀ y ∈ B C = D ↔ ∀ z z = C ↔ z = D → ∀ y ∈ B C = D ↔ ∀ y ∈ B ∀ z z = C ↔ z = D
16 14 15 syl ⊢ ∀ y ∈ B C ∈ V → ∀ y ∈ B C = D ↔ ∀ y ∈ B ∀ z z = C ↔ z = D
17 16 ralimi ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → ∀ x ∈ A ∀ y ∈ B C = D ↔ ∀ y ∈ B ∀ z z = C ↔ z = D
18 ralbi ⊢ ∀ x ∈ A ∀ y ∈ B C = D ↔ ∀ y ∈ B ∀ z z = C ↔ z = D → ∀ x ∈ A ∀ y ∈ B C = D ↔ ∀ x ∈ A ∀ y ∈ B ∀ z z = C ↔ z = D
19 17 18 syl ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → ∀ x ∈ A ∀ y ∈ B C = D ↔ ∀ x ∈ A ∀ y ∈ B ∀ z z = C ↔ z = D
20 12 19 bitr4id ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → x ∈ A , y ∈ B ⟼ C = x ∈ A , y ∈ B ⟼ D ↔ ∀ x ∈ A ∀ y ∈ B C = D