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

Theorem inrab 3932
 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 2950 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 df-rab 2950 . . 3 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
31, 2ineq12i 3845 . 2 ({𝑥𝐴𝜑} ∩ {𝑥𝐴𝜓}) = ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)})
4 df-rab 2950 . . 3 {𝑥𝐴 ∣ (𝜑𝜓)} = {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))}
5 inab 3928 . . . 4 ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)}) = {𝑥 ∣ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓))}
6 anandi 888 . . . . 5 ((𝑥𝐴 ∧ (𝜑𝜓)) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓)))
76abbii 2768 . . . 4 {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))} = {𝑥 ∣ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓))}
85, 7eqtr4i 2676 . . 3 ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)}) = {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))}
94, 8eqtr4i 2676 . 2 {𝑥𝐴 ∣ (𝜑𝜓)} = ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)})
103, 9eqtr4i 2676 1 ({𝑥𝐴𝜑} ∩ {𝑥𝐴𝜓}) = {𝑥𝐴 ∣ (𝜑𝜓)}
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   = wceq 1523   ∈ wcel 2030  {cab 2637  {crab 2945   ∩ cin 3606 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-in 3614 This theorem is referenced by:  rabnc  3995  ixxin  12230  hashbclem  13274  phiprmpw  15528  submacs  17412  ablfacrp  18511  dfrhm2  18765  ordtbaslem  21040  ordtbas2  21043  ordtopn3  21048  ordtcld3  21051  ordthauslem  21235  pthaus  21489  xkohaus  21504  tsmsfbas  21978  minveclem3b  23245  shftmbl  23352  mumul  24952  ppiub  24974  lgsquadlem2  25151  umgrislfupgrlem  26062  numedglnl  26084  clwwlknondisj  27086  clwwlknondisjOLD  27090  frcond3  27249  numclwwlk3lemOLD  27369  numclwwlk3lem  27371  xppreima  29577  xpinpreima  30080  xpinpreima2  30081  measvuni  30405  subfacp1lem6  31293  cnambfre  33588  itg2addnclem2  33592  ftc1anclem6  33620  refsymrels2  34449  anrabdioph  37661  undisjrab  38822  smfaddlem2  41293  smfmullem4  41322
 Copyright terms: Public domain W3C validator