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

Theorem inrab 4042
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 3059 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 df-rab 3059 . . 3 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
31, 2ineq12i 3955 . 2 ({𝑥𝐴𝜑} ∩ {𝑥𝐴𝜓}) = ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)})
4 df-rab 3059 . . 3 {𝑥𝐴 ∣ (𝜑𝜓)} = {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))}
5 inab 4038 . . . 4 ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)}) = {𝑥 ∣ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓))}
6 anandi 906 . . . . 5 ((𝑥𝐴 ∧ (𝜑𝜓)) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓)))
76abbii 2877 . . . 4 {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))} = {𝑥 ∣ ((𝑥𝐴𝜑) ∧ (𝑥𝐴𝜓))}
85, 7eqtr4i 2785 . . 3 ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)}) = {𝑥 ∣ (𝑥𝐴 ∧ (𝜑𝜓))}
94, 8eqtr4i 2785 . 2 {𝑥𝐴 ∣ (𝜑𝜓)} = ({𝑥 ∣ (𝑥𝐴𝜑)} ∩ {𝑥 ∣ (𝑥𝐴𝜓)})
103, 9eqtr4i 2785 1 ({𝑥𝐴𝜑} ∩ {𝑥𝐴𝜓}) = {𝑥𝐴 ∣ (𝜑𝜓)}
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1632  wcel 2139  {cab 2746  {crab 3054  cin 3714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-in 3722
This theorem is referenced by:  rabnc  4105  ixxin  12405  hashbclem  13448  phiprmpw  15703  submacs  17586  ablfacrp  18685  dfrhm2  18939  ordtbaslem  21214  ordtbas2  21217  ordtopn3  21222  ordtcld3  21225  ordthauslem  21409  pthaus  21663  xkohaus  21678  tsmsfbas  22152  minveclem3b  23419  shftmbl  23526  mumul  25127  ppiub  25149  lgsquadlem2  25326  umgrislfupgrlem  26237  numedglnl  26259  clwwlknondisj  27281  clwwlknondisjOLD  27285  frcond3  27444  numclwwlk3lemOLD  27571  numclwwlk3lem  27573  xppreima  29779  xpinpreima  30282  xpinpreima2  30283  measvuni  30607  subfacp1lem6  31495  cnambfre  33789  itg2addnclem2  33793  ftc1anclem6  33821  refsymrels2  34652  anrabdioph  37864  undisjrab  39025  smfaddlem2  41496  smfmullem4  41525
  Copyright terms: Public domain W3C validator