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

Theorem inrab 3858
 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 2905 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 df-rab 2905 . . 3 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
31, 2ineq12i 3774 . 2 ({𝑥𝐴𝜑} ∩ {𝑥𝐴𝜓}) = ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)})
4 df-rab 2905 . . 3 {𝑥𝐴 ∣ (𝜑𝜓)} = {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))}
5 inab 3854 . . . 4 ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)}) = {𝑥 ∣ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓))}
6 anandi 867 . . . . 5 ((𝑥𝐴 ∧ (𝜑𝜓)) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓)))
76abbii 2726 . . . 4 {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))} = {𝑥 ∣ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓))}
85, 7eqtr4i 2635 . . 3 ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)}) = {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))}
94, 8eqtr4i 2635 . 2 {𝑥𝐴 ∣ (𝜑𝜓)} = ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)})
103, 9eqtr4i 2635 1 ({𝑥𝐴𝜑} ∩ {𝑥𝐴𝜓}) = {𝑥𝐴 ∣ (𝜑𝜓)}
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596  {crab 2900   ∩ cin 3539 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-in 3547 This theorem is referenced by:  rabnc  3916  ixxin  12063  hashbclem  13093  phiprmpw  15319  submacs  17188  ablfacrp  18288  dfrhm2  18540  ordtbaslem  20802  ordtbas2  20805  ordtopn3  20810  ordtcld3  20813  ordthauslem  20997  pthaus  21251  xkohaus  21266  tsmsfbas  21741  minveclem3b  23007  shftmbl  23113  mumul  24707  ppiub  24729  lgsquadlem2  24906  umgrislfupgrlem  25788  cusgrasizeindslem1  26002  frisusgranb  26524  numclwwlkdisj  26607  numclwwlk3lem  26635  xppreima  28829  xpinpreima  29280  xpinpreima2  29281  measvuni  29604  subfacp1lem6  30421  cnambfre  32628  itg2addnclem2  32632  ftc1anclem6  32660  anrabdioph  36362  undisjrab  37527  smfaddlem2  39650  smfmullem4  39679  clwwlksndisj  41280  frcond3  41440  av-numclwwlk3lem  41538
 Copyright terms: Public domain W3C validator