Theorem reqabi 3440

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

Hypothesis

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

Assertion

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

Proof of Theorem reqabi

Step	Hyp	Ref	Expression
1		reqabi.1	. . 3 ⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑}
2	1	eleq2i 2857	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑})
3		rabid 3438	. 2 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	2, 3	bitri 278	1 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1563   ∈ wcel 2145  {crab 3417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418

This theorem is referenced by:  fvmptss  6992  tfis  7839  nqereu  10902  rpnnen1lem2  12989  rpnnen1lem1  12990  rpnnen1lem3  12991  rpnnen1lem5  12993  qustgpopn  24234  nbusgrf1o0  29624  finsumvtxdg2ssteplem3  29802  frgrwopreglem2  30569  frgrwopreglem5lem  30576  partfun2  32929  resf1o  32983  elrgspnlem4  33473  nsgqusf1olem2  33634  nsgqusf1olem3  33635  ballotlem2  34791  reprsuc  34914  oddprm2  34954  hgt750lemb  34955  bnj1476  35147  bnj1533  35152  bnj1538  35155  bnj1523  35371  cvmlift2lem12  35672  neibastop2lem  36728  topdifinfindis  37847  topdifinffinlem  37848  stoweidlem24  46597  stoweidlem31  46604  stoweidlem52  46625  stoweidlem54  46627  stoweidlem57  46630  salexct  46907  ovolval5lem3  47227  pimdecfgtioc  47288  pimincfltioc  47289  pimdecfgtioo  47290  pimincfltioo  47291  smfsuplem1  47384  smfsuplem3  47386  smfliminflem  47403  prprsprreu  48124