Theorem rabeq2i 3398

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 3290	. 2 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	2, 3	bitri 278	1 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2110  {crab 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070

This theorem is referenced by:  fvmptss  6830  tfis  7633  nqereu  10543  rpnnen1lem2  12573  rpnnen1lem1  12574  rpnnen1lem3  12575  rpnnen1lem5  12577  qustgpopn  23017  nbusgrf1o0  27457  finsumvtxdg2ssteplem3  27635  frgrwopreglem2  28396  frgrwopreglem5lem  28403  resf1o  30785  nsgqusf1olem2  31313  nsgqusf1olem3  31314  ballotlem2  32167  reprsuc  32307  oddprm2  32347  hgt750lemb  32348  bnj1476  32540  bnj1533  32545  bnj1538  32548  bnj1523  32764  cvmlift2lem12  32989  neibastop2lem  34286  topdifinfindis  35254  topdifinffinlem  35255  stoweidlem24  43240  stoweidlem31  43247  stoweidlem52  43268  stoweidlem54  43270  stoweidlem57  43273  salexct  43548  ovolval5lem3  43867  pimdecfgtioc  43924  pimincfltioc  43925  pimdecfgtioo  43926  pimincfltioo  43927  smfsuplem1  44016  smfsuplem3  44018  smfliminflem  44035  prprsprreu  44644