Theorem reqabi 3412

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {crab 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390

This theorem is referenced by:  fvmptss  6960  tfis  7806  nqereu  10852  rpnnen1lem2  12927  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem5  12931  qustgpopn  24085  nbusgrf1o0  29438  finsumvtxdg2ssteplem3  29616  frgrwopreglem2  30383  frgrwopreglem5lem  30390  partfun2  32749  resf1o  32803  elrgspnlem4  33306  nsgqusf1olem2  33474  nsgqusf1olem3  33475  ballotlem2  34633  reprsuc  34759  oddprm2  34799  hgt750lemb  34800  bnj1476  34989  bnj1533  34994  bnj1538  34997  bnj1523  35213  cvmlift2lem12  35496  neibastop2lem  36542  topdifinfindis  37662  topdifinffinlem  37663  stoweidlem24  46452  stoweidlem31  46459  stoweidlem52  46480  stoweidlem54  46482  stoweidlem57  46485  salexct  46762  ovolval5lem3  47082  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  smfsuplem1  47239  smfsuplem3  47241  smfliminflem  47258  prprsprreu  47979