Theorem rabeq2i 3426

Description: Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.)

Hypothesis

Ref	Expression
rabeq2i.1	⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑}

Assertion

Ref	Expression
rabeq2i	⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))

Proof of Theorem rabeq2i

Step	Hyp	Ref	Expression
1		rabeq2i.1	. . 3 ⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑}
2	1	eleq2i 2829	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑})
3		rabid 3424	. 2 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	2, 3	bitri 275	1 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))

Syntax hints:   ↔ wb 205   ∧ wa 397   = wceq 1541   ∈ wcel 2106  {crab 3404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405

This theorem is referenced by:  fvmptss  6948  tfis  7774  nqereu  10791  rpnnen1lem2  12823  rpnnen1lem1  12824  rpnnen1lem3  12825  rpnnen1lem5  12827  qustgpopn  23377  nbusgrf1o0  28025  finsumvtxdg2ssteplem3  28203  frgrwopreglem2  28965  frgrwopreglem5lem  28972  resf1o  31350  nsgqusf1olem2  31894  nsgqusf1olem3  31895  ballotlem2  32753  reprsuc  32893  oddprm2  32933  hgt750lemb  32934  bnj1476  33124  bnj1533  33129  bnj1538  33132  bnj1523  33348  cvmlift2lem12  33573  addsproplem2  34234  sleadd1  34250  neibastop2lem  34686  topdifinfindis  35671  topdifinffinlem  35672  stoweidlem24  43951  stoweidlem31  43958  stoweidlem52  43979  stoweidlem54  43981  stoweidlem57  43984  salexct  44259  ovolval5lem3  44579  pimdecfgtioc  44640  pimincfltioc  44641  pimdecfgtioo  44642  pimincfltioo  44643  smfsuplem1  44736  smfsuplem3  44738  smfliminflem  44755  prprsprreu  45387