Theorem reqabi 3420

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

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

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 3397

This theorem is referenced by:  fvmptss  6946  tfis  7795  nqereu  10842  rpnnen1lem2  12896  rpnnen1lem1  12897  rpnnen1lem3  12898  rpnnen1lem5  12900  qustgpopn  24023  nbusgrf1o0  29332  finsumvtxdg2ssteplem3  29511  frgrwopreglem2  30275  frgrwopreglem5lem  30282  resf1o  32686  elrgspnlem4  33195  nsgqusf1olem2  33361  nsgqusf1olem3  33362  ballotlem2  34456  reprsuc  34582  oddprm2  34622  hgt750lemb  34623  bnj1476  34813  bnj1533  34818  bnj1538  34821  bnj1523  35037  cvmlift2lem12  35286  neibastop2lem  36333  topdifinfindis  37319  topdifinffinlem  37320  stoweidlem24  46006  stoweidlem31  46013  stoweidlem52  46034  stoweidlem54  46036  stoweidlem57  46039  salexct  46316  ovolval5lem3  46636  pimdecfgtioc  46697  pimincfltioc  46698  pimdecfgtioo  46699  pimincfltioo  46700  smfsuplem1  46793  smfsuplem3  46795  smfliminflem  46812  prprsprreu  47504