Theorem inrab 3858

Description: Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.)

Assertion

Ref	Expression
inrab	⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}

Proof of Theorem inrab

Step	Hyp	Ref	Expression
1		df-rab 2905	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
2		df-rab 2905	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}
3	1, 2	ineq12i 3774	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
4		df-rab 2905	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))}
5		inab 3854	. . . 4 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))}
6		anandi 867	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)))
7	6	abbii 2726	. . . 4 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))} = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))}
8	5, 7	eqtr4i 2635	. . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))}
9	4, 8	eqtr4i 2635	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)})
10	3, 9	eqtr4i 2635	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}

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