Metamath Proof Explorer

Theorem eqoprab2bw

Description: Equivalence of ordered pair abstraction subclass and biconditional. Version of eqoprab2b with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 4-Jan-2017) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

Ref Expression
Assertion eqoprab2bw ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 nfoprab1 ⊢ Ⅎ 𝑥 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
2 nfoprab1 ⊢ Ⅎ 𝑥 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 }
3 1 2 nfss ⊢ Ⅎ 𝑥 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 }
4 nfoprab2 ⊢ Ⅎ 𝑦 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
5 nfoprab2 ⊢ Ⅎ 𝑦 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 }
6 4 5 nfss ⊢ Ⅎ 𝑦 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 }
7 nfoprab3 ⊢ Ⅎ 𝑧 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
8 nfoprab3 ⊢ Ⅎ 𝑧 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 }
9 7 8 nfss ⊢ Ⅎ 𝑧 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 }
10 ssel ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } → ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ) )
11 oprabidw ⊢ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ 𝜑 )
12 oprabidw ⊢ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ↔ 𝜓 )
13 10 11 12 3imtr3g ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } → ( 𝜑 → 𝜓 ) )
14 9 13 alrimi ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } → ∀ 𝑧 ( 𝜑 → 𝜓 ) )
15 6 14 alrimi ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } → ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) )
16 3 15 alrimi ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) )
17 ssoprab2 ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } )
18 16 17 impbii ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) )
19 2 1 nfss ⊢ Ⅎ 𝑥 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
20 5 4 nfss ⊢ Ⅎ 𝑦 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
21 8 7 nfss ⊢ Ⅎ 𝑧 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
22 ssel ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } → ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ) )
23 22 12 11 3imtr3g ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → ( 𝜓 → 𝜑 ) )
24 21 23 alrimi ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → ∀ 𝑧 ( 𝜓 → 𝜑 ) )
25 20 24 alrimi ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) )
26 19 25 alrimi ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) )
27 ssoprab2 ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } )
28 26 27 impbii ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) )
29 18 28 anbi12i ⊢ ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ∧ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ) ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) ) )
30 eqss ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ↔ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ∧ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ) )
31 2albiim ⊢ ( ∀ 𝑦 ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) ↔ ( ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) ) )
32 31 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) ↔ ∀ 𝑥 ( ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) ) )
33 19.26 ⊢ ( ∀ 𝑥 ( ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) ) ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) ) )
34 32 33 bitri ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) ) )
35 29 30 34 3bitr4i ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) )