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

Theorem inrab 4063
Description: Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.)
Assertion
Ref Expression
inrab ({𝑥𝐴𝜑} ∩ {𝑥𝐴𝜓}) = {𝑥𝐴 ∣ (𝜑𝜓)}

Proof of Theorem inrab
StepHypRef Expression
1 df-rab 3064 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 df-rab 3064 . . 3 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
31, 2ineq12i 3974 . 2 ({𝑥𝐴𝜑} ∩ {𝑥𝐴𝜓}) = ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)})
4 df-rab 3064 . . 3 {𝑥𝐴 ∣ (𝜑𝜓)} = {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))}
5 inab 4059 . . . 4 ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)}) = {𝑥 ∣ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓))}
6 anandi 666 . . . . 5 ((𝑥𝐴 ∧ (𝜑𝜓)) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓)))
76abbii 2882 . . . 4 {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))} = {𝑥 ∣ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓))}
85, 7eqtr4i 2790 . . 3 ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)}) = {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))}
94, 8eqtr4i 2790 . 2 {𝑥𝐴 ∣ (𝜑𝜓)} = ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)})
103, 9eqtr4i 2790 1 ({𝑥𝐴𝜑} ∩ {𝑥𝐴𝜓}) = {𝑥𝐴 ∣ (𝜑𝜓)}
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1652  wcel 2155  {cab 2751  {crab 3059  cin 3731
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rab 3064  df-v 3352  df-in 3739
This theorem is referenced by:  rabnc  4124  ixxin  12394  hashbclem  13437  phiprmpw  15762  submacs  17633  ablfacrp  18732  dfrhm2  18986  ordtbaslem  21272  ordtbas2  21275  ordtopn3  21280  ordtcld3  21283  ordthauslem  21467  pthaus  21721  xkohaus  21736  tsmsfbas  22210  minveclem3b  23488  shftmbl  23596  mumul  25198  ppiub  25220  lgsquadlem2  25397  umgrislfupgrlem  26294  numedglnl  26317  clwwlknondisj  27343  clwwlknondisjOLD  27348  frcond3  27507  numclwwlk3lemOLD  27632  numclwwlk3lem2  27635  xppreima  29834  xpinpreima  30334  xpinpreima2  30335  measvuni  30659  subfacp1lem6  31547  cnambfre  33813  itg2addnclem2  33817  ftc1anclem6  33845  refsymrels2  34672  dfeqvrels2  34693  refrelsred4  34734  anrabdioph  37954  undisjrab  39111  smfaddlem2  41544  smfmullem4  41573
  Copyright terms: Public domain W3C validator