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

Theorem inopab 5448
Description: Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
Assertion
Ref Expression
inopab ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∩ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑𝜓)}
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem inopab
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relopab 5443 . . 3 Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2 relin1 5431 . . 3 (Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑} → Rel ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∩ {⟨𝑥, 𝑦⟩ ∣ 𝜓}))
31, 2ax-mp 5 . 2 Rel ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∩ {⟨𝑥, 𝑦⟩ ∣ 𝜓})
4 relopab 5443 . 2 Rel {⟨𝑥, 𝑦⟩ ∣ (𝜑𝜓)}
5 sban 2557 . . . 4 ([𝑤 / 𝑦]([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝜓) ↔ ([𝑤 / 𝑦][𝑧 / 𝑥]𝜑 ∧ [𝑤 / 𝑦][𝑧 / 𝑥]𝜓))
6 sban 2557 . . . . 5 ([𝑧 / 𝑥](𝜑𝜓) ↔ ([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝜓))
76sbbii 2066 . . . 4 ([𝑤 / 𝑦][𝑧 / 𝑥](𝜑𝜓) ↔ [𝑤 / 𝑦]([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝜓))
8 opelopabsbALT 5173 . . . . 5 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑)
9 opelopabsbALT 5173 . . . . 5 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜓)
108, 9anbi12i 614 . . . 4 ((⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∧ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) ↔ ([𝑤 / 𝑦][𝑧 / 𝑥]𝜑 ∧ [𝑤 / 𝑦][𝑧 / 𝑥]𝜓))
115, 7, 103bitr4ri 295 . . 3 ((⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∧ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) ↔ [𝑤 / 𝑦][𝑧 / 𝑥](𝜑𝜓))
12 elin 3989 . . 3 (⟨𝑧, 𝑤⟩ ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∩ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) ↔ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ∧ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓}))
13 opelopabsbALT 5173 . . 3 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝜑𝜓)} ↔ [𝑤 / 𝑦][𝑧 / 𝑥](𝜑𝜓))
1411, 12, 133bitr4i 294 . 2 (⟨𝑧, 𝑤⟩ ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∩ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝜑𝜓)})
153, 4, 14eqrelriiv 5410 1 ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∩ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑𝜓)}
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1637  [wsb 2059  wcel 2155  cin 3762  cop 4370  {copab 4899  Rel wrel 5310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pr 5090
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-rab 3101  df-v 3389  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-sn 4365  df-pr 4367  df-op 4371  df-opab 4900  df-xp 5311  df-rel 5312
This theorem is referenced by:  inxp  5450  resopab  5645  fndmin  6540  cnvoprab  7456  epinid0  8738  cnvepnep  8744  wemapwe  8835  dfiso2  16630  frgpuplem  18380  ltbwe  19675  opsrtoslem1  19686  pjfval2  20257  lgsquadlem3  25315  br1cosscnvxrn  34531  1cosscnvxrn  34532  dnwech  38113  fgraphopab  38283
  Copyright terms: Public domain W3C validator