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 pm13.183 ⊢ C ∈ V → C = D ↔ ∀ z z = C ↔ z = D
2 1 ralimi ⊢ ∀ y ∈ B C ∈ V → ∀ y ∈ B C = D ↔ ∀ z z = C ↔ z = D
3 ralbi ⊢ ∀ y ∈ B C = D ↔ ∀ z z = C ↔ z = D → ∀ y ∈ B C = D ↔ ∀ y ∈ B ∀ z z = C ↔ z = D
4 2 3 syl ⊢ ∀ y ∈ B C ∈ V → ∀ y ∈ B C = D ↔ ∀ y ∈ B ∀ z z = C ↔ z = D
5 4 ralimi ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → ∀ x ∈ A ∀ y ∈ B C = D ↔ ∀ y ∈ B ∀ z z = C ↔ z = D
6 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
7 5 6 syl ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → ∀ x ∈ A ∀ y ∈ B C = D ↔ ∀ x ∈ A ∀ y ∈ B ∀ z z = C ↔ z = D
8 df-mpo ⊢ x ∈ A , y ∈ B ⟼ C = x y z | x ∈ A ∧ y ∈ B ∧ z = C
9 df-mpo ⊢ x ∈ A , y ∈ B ⟼ D = x y z | x ∈ A ∧ y ∈ B ∧ z = D
10 8 9 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
11 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
12 pm5.32 ⊢ x ∈ A ∧ y ∈ B → z = C ↔ z = D ↔ x ∈ A ∧ y ∈ B ∧ z = C ↔ x ∈ A ∧ y ∈ B ∧ z = D
13 12 albii ⊢ ∀ z x ∈ A ∧ y ∈ B → z = C ↔ z = D ↔ ∀ z x ∈ A ∧ y ∈ B ∧ z = C ↔ x ∈ A ∧ y ∈ B ∧ z = D
14 19.21v ⊢ ∀ z x ∈ A ∧ y ∈ B → z = C ↔ z = D ↔ x ∈ A ∧ y ∈ B → ∀ z z = C ↔ z = D
15 13 14 bitr3i ⊢ ∀ z x ∈ A ∧ y ∈ B ∧ z = C ↔ x ∈ A ∧ y ∈ B ∧ z = D ↔ x ∈ A ∧ y ∈ B → ∀ z z = C ↔ z = D
16 15 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
17 r2al ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z z = C ↔ z = D ↔ ∀ x ∀ y x ∈ A ∧ y ∈ B → ∀ z z = C ↔ z = D
18 16 17 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
19 10 11 18 3bitri ⊢ x ∈ A , y ∈ B ⟼ C = x ∈ A , y ∈ B ⟼ D ↔ ∀ x ∈ A ∀ y ∈ B ∀ z z = C ↔ z = D
20 7 19 syl6rbbr ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ V → x ∈ A , y ∈ B ⟼ C = x ∈ A , y ∈ B ⟼ D ↔ ∀ x ∈ A ∀ y ∈ B C = D