Theorem rabeq2i 3490

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

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1536   ∈ wcel 2113  {crab 3145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1539  df-ex 1780  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3150

This theorem is referenced by:  fvmptss  6783  tfis  7572  nqereu  10354  rpnnen1lem2  12379  rpnnen1lem1  12380  rpnnen1lem3  12381  rpnnen1lem5  12383  qustgpopn  22731  nbusgrf1o0  27154  finsumvtxdg2ssteplem3  27332  frgrwopreglem2  28095  frgrwopreglem5lem  28102  resf1o  30469  ballotlem2  31750  reprsuc  31890  oddprm2  31930  hgt750lemb  31931  bnj1476  32123  bnj1533  32128  bnj1538  32131  bnj1523  32347  cvmlift2lem12  32565  neibastop2lem  33712  topdifinfindis  34631  topdifinffinlem  34632  stoweidlem24  42316  stoweidlem31  42323  stoweidlem52  42344  stoweidlem54  42346  stoweidlem57  42349  salexct  42624  ovolval5lem3  42943  pimdecfgtioc  43000  pimincfltioc  43001  pimdecfgtioo  43002  pimincfltioo  43003  smfsuplem1  43092  smfsuplem3  43094  smfliminflem  43111  prprsprreu  43688