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

Theorem inrab 4237
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 3072 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 df-rab 3072 . . 3 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
31, 2ineq12i 4141 . 2 ({𝑥𝐴𝜑} ∩ {𝑥𝐴𝜓}) = ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)})
4 df-rab 3072 . . 3 {𝑥𝐴 ∣ (𝜑𝜓)} = {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))}
5 inab 4230 . . . 4 ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)}) = {𝑥 ∣ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓))}
6 anandi 672 . . . . 5 ((𝑥𝐴 ∧ (𝜑𝜓)) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓)))
76abbii 2809 . . . 4 {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))} = {𝑥 ∣ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓))}
85, 7eqtr4i 2769 . . 3 ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)}) = {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))}
94, 8eqtr4i 2769 . 2 {𝑥𝐴 ∣ (𝜑𝜓)} = ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)})
103, 9eqtr4i 2769 1 ({𝑥𝐴𝜑} ∩ {𝑥𝐴𝜓}) = {𝑥𝐴 ∣ (𝜑𝜓)}
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1539  wcel 2108  {cab 2715  {crab 3067  cin 3882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890
This theorem is referenced by:  rabnc  4318  ixxin  13025  hashbclem  14092  phiprmpw  16405  submacs  18380  ablfacrp  19584  dfrhm2  19876  ordtbaslem  22247  ordtbas2  22250  ordtopn3  22255  ordtcld3  22258  ordthauslem  22442  pthaus  22697  xkohaus  22712  tsmsfbas  23187  minveclem3b  24497  shftmbl  24607  mumul  26235  ppiub  26257  lgsquadlem2  26434  umgrislfupgrlem  27395  numedglnl  27417  clwwlknondisj  28376  frcond3  28534  numclwwlk3lem2  28649  xppreima  30884  xpinpreima  31758  xpinpreima2  31759  measvuni  32082  subfacp1lem6  33047  satfv1  33225  cnambfre  35752  itg2addnclem2  35756  ftc1anclem6  35782  refsymrels2  36606  dfeqvrels2  36628  refrelsredund4  36672  anrabdioph  40518  undisjrab  41813  smfaddlem2  44186  smfmullem4  44215
  Copyright terms: Public domain W3C validator