Theorem reqabi 3415

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

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {crab 3392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-12 2189  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393

This theorem is referenced by:  fvmptss  6955  tfis  7802  nqereu  10850  rpnnen1lem2  12925  rpnnen1lem1  12926  rpnnen1lem3  12927  rpnnen1lem5  12929  qustgpopn  24110  nbusgrf1o0  29463  finsumvtxdg2ssteplem3  29641  frgrwopreglem2  30408  frgrwopreglem5lem  30415  partfun2  32775  resf1o  32829  elrgspnlem4  33333  nsgqusf1olem2  33504  nsgqusf1olem3  33505  ballotlem2  34680  reprsuc  34806  oddprm2  34846  hgt750lemb  34847  bnj1476  35036  bnj1533  35041  bnj1538  35044  bnj1523  35260  cvmlift2lem12  35549  neibastop2lem  36595  topdifinfindis  37715  topdifinffinlem  37716  stoweidlem24  46474  stoweidlem31  46481  stoweidlem52  46502  stoweidlem54  46504  stoweidlem57  46507  salexct  46784  ovolval5lem3  47104  pimdecfgtioc  47165  pimincfltioc  47166  pimdecfgtioo  47167  pimincfltioo  47168  smfsuplem1  47261  smfsuplem3  47263  smfliminflem  47280  prprsprreu  48001