Theorem reqabi 3418

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {crab 3395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396

This theorem is referenced by:  fvmptss  6941  tfis  7785  nqereu  10817  rpnnen1lem2  12872  rpnnen1lem1  12873  rpnnen1lem3  12874  rpnnen1lem5  12876  qustgpopn  24033  nbusgrf1o0  29345  finsumvtxdg2ssteplem3  29524  frgrwopreglem2  30288  frgrwopreglem5lem  30295  resf1o  32708  elrgspnlem4  33207  nsgqusf1olem2  33374  nsgqusf1olem3  33375  ballotlem2  34497  reprsuc  34623  oddprm2  34663  hgt750lemb  34664  bnj1476  34854  bnj1533  34859  bnj1538  34862  bnj1523  35078  cvmlift2lem12  35346  neibastop2lem  36393  topdifinfindis  37379  topdifinffinlem  37380  stoweidlem24  46061  stoweidlem31  46068  stoweidlem52  46089  stoweidlem54  46091  stoweidlem57  46094  salexct  46371  ovolval5lem3  46691  pimdecfgtioc  46752  pimincfltioc  46753  pimdecfgtioo  46754  pimincfltioo  46755  smfsuplem1  46848  smfsuplem3  46850  smfliminflem  46867  prprsprreu  47549