Theorem reqabi 3429

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {crab 3405

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406

This theorem is referenced by:  fvmptss  6980  tfis  7831  nqereu  10882  rpnnen1lem2  12936  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  qustgpopn  24007  nbusgrf1o0  29296  finsumvtxdg2ssteplem3  29475  frgrwopreglem2  30242  frgrwopreglem5lem  30249  resf1o  32653  elrgspnlem4  33196  nsgqusf1olem2  33385  nsgqusf1olem3  33386  ballotlem2  34480  reprsuc  34606  oddprm2  34646  hgt750lemb  34647  bnj1476  34837  bnj1533  34842  bnj1538  34845  bnj1523  35061  cvmlift2lem12  35301  neibastop2lem  36348  topdifinfindis  37334  topdifinffinlem  37335  stoweidlem24  46022  stoweidlem31  46029  stoweidlem52  46050  stoweidlem54  46052  stoweidlem57  46055  salexct  46332  ovolval5lem3  46652  pimdecfgtioc  46713  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  smfsuplem1  46809  smfsuplem3  46811  smfliminflem  46828  prprsprreu  47520