Theorem rabeq2i 3412

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

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {crab 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072

This theorem is referenced by:  fvmptss  6869  tfis  7676  nqereu  10616  rpnnen1lem2  12646  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  qustgpopn  23179  nbusgrf1o0  27639  finsumvtxdg2ssteplem3  27817  frgrwopreglem2  28578  frgrwopreglem5lem  28585  resf1o  30967  nsgqusf1olem2  31501  nsgqusf1olem3  31502  ballotlem2  32355  reprsuc  32495  oddprm2  32535  hgt750lemb  32536  bnj1476  32727  bnj1533  32732  bnj1538  32735  bnj1523  32951  cvmlift2lem12  33176  neibastop2lem  34476  topdifinfindis  35444  topdifinffinlem  35445  stoweidlem24  43455  stoweidlem31  43462  stoweidlem52  43483  stoweidlem54  43485  stoweidlem57  43488  salexct  43763  ovolval5lem3  44082  pimdecfgtioc  44139  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  smfsuplem1  44231  smfsuplem3  44233  smfliminflem  44250  prprsprreu  44859