Theorem rabeq2i 3424

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

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1537   ∈ wcel 2101  {crab 3221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-12 2166  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1540  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3224

This theorem is referenced by:  fvmptss  6907  tfis  7721  nqereu  10713  rpnnen1lem2  12745  rpnnen1lem1  12746  rpnnen1lem3  12747  rpnnen1lem5  12749  qustgpopn  23299  nbusgrf1o0  27764  finsumvtxdg2ssteplem3  27942  frgrwopreglem2  28705  frgrwopreglem5lem  28712  resf1o  31093  nsgqusf1olem2  31627  nsgqusf1olem3  31628  ballotlem2  32483  reprsuc  32623  oddprm2  32663  hgt750lemb  32664  bnj1476  32855  bnj1533  32860  bnj1538  32863  bnj1523  33079  cvmlift2lem12  33304  neibastop2lem  34577  topdifinfindis  35545  topdifinffinlem  35546  stoweidlem24  43600  stoweidlem31  43607  stoweidlem52  43628  stoweidlem54  43630  stoweidlem57  43633  salexct  43908  ovolval5lem3  44228  pimdecfgtioc  44289  pimincfltioc  44290  pimdecfgtioo  44291  pimincfltioo  44292  smfsuplem1  44384  smfsuplem3  44386  smfliminflem  44403  prprsprreu  45011