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∈BC∈V→x∈A,y∈B⟼C=x∈A,y∈B⟼D↔∀x∈A∀y∈BC=D

Proof

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