MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqoprab2bw Structured version   Visualization version   GIF version

Theorem eqoprab2bw 7281
Description: Equivalence of ordered pair abstraction subclass and biconditional. Version of eqoprab2b 7282 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Mario Carneiro, 4-Jan-2017.) (Revised by Gino Giotto, 26-Jan-2024.)
Assertion
Ref Expression
eqoprab2bw ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥𝑦𝑧(𝜑𝜓))
Distinct variable group:   𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝜓(𝑥,𝑦,𝑧)

Proof of Theorem eqoprab2bw
StepHypRef Expression
1 nfoprab1 7272 . . . . . 6 𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
2 nfoprab1 7272 . . . . . 6 𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
31, 2nfss 3892 . . . . 5 𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
4 nfoprab2 7273 . . . . . . 7 𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
5 nfoprab2 7273 . . . . . . 7 𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
64, 5nfss 3892 . . . . . 6 𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
7 nfoprab3 7274 . . . . . . . 8 𝑧{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
8 nfoprab3 7274 . . . . . . . 8 𝑧{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
97, 8nfss 3892 . . . . . . 7 𝑧{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}
10 ssel 3893 . . . . . . . 8 ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} → (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} → ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓}))
11 oprabidw 7244 . . . . . . . 8 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)
12 oprabidw 7244 . . . . . . . 8 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ 𝜓)
1310, 11, 123imtr3g 298 . . . . . . 7 ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} → (𝜑𝜓))
149, 13alrimi 2211 . . . . . 6 ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} → ∀𝑧(𝜑𝜓))
156, 14alrimi 2211 . . . . 5 ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} → ∀𝑦𝑧(𝜑𝜓))
163, 15alrimi 2211 . . . 4 ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} → ∀𝑥𝑦𝑧(𝜑𝜓))
17 ssoprab2 7279 . . . 4 (∀𝑥𝑦𝑧(𝜑𝜓) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓})
1816, 17impbii 212 . . 3 ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥𝑦𝑧(𝜑𝜓))
192, 1nfss 3892 . . . . 5 𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
205, 4nfss 3892 . . . . . 6 𝑦{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
218, 7nfss 3892 . . . . . . 7 𝑧{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
22 ssel 3893 . . . . . . . 8 ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} → (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} → ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}))
2322, 12, 113imtr3g 298 . . . . . . 7 ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} → (𝜓𝜑))
2421, 23alrimi 2211 . . . . . 6 ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} → ∀𝑧(𝜓𝜑))
2520, 24alrimi 2211 . . . . 5 ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} → ∀𝑦𝑧(𝜓𝜑))
2619, 25alrimi 2211 . . . 4 ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} → ∀𝑥𝑦𝑧(𝜓𝜑))
27 ssoprab2 7279 . . . 4 (∀𝑥𝑦𝑧(𝜓𝜑) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑})
2826, 27impbii 212 . . 3 ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ ∀𝑥𝑦𝑧(𝜓𝜑))
2918, 28anbi12i 630 . 2 (({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ∧ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}) ↔ (∀𝑥𝑦𝑧(𝜑𝜓) ∧ ∀𝑥𝑦𝑧(𝜓𝜑)))
30 eqss 3916 . 2 ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ∧ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ⊆ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}))
31 2albiim 1898 . . . 4 (∀𝑦𝑧(𝜑𝜓) ↔ (∀𝑦𝑧(𝜑𝜓) ∧ ∀𝑦𝑧(𝜓𝜑)))
3231albii 1827 . . 3 (∀𝑥𝑦𝑧(𝜑𝜓) ↔ ∀𝑥(∀𝑦𝑧(𝜑𝜓) ∧ ∀𝑦𝑧(𝜓𝜑)))
33 19.26 1878 . . 3 (∀𝑥(∀𝑦𝑧(𝜑𝜓) ∧ ∀𝑦𝑧(𝜓𝜑)) ↔ (∀𝑥𝑦𝑧(𝜑𝜓) ∧ ∀𝑥𝑦𝑧(𝜓𝜑)))
3432, 33bitri 278 . 2 (∀𝑥𝑦𝑧(𝜑𝜓) ↔ (∀𝑥𝑦𝑧(𝜑𝜓) ∧ ∀𝑥𝑦𝑧(𝜓𝜑)))
3529, 30, 343bitr4i 306 1 ({⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} ↔ ∀𝑥𝑦𝑧(𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1541   = wceq 1543  wcel 2110  wss 3866  cop 4547  {coprab 7214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-oprab 7217
This theorem is referenced by:  mpo2eqb  7342
  Copyright terms: Public domain W3C validator