Theorem reqabi 3439

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

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417

This theorem is referenced by:  fvmptss  7004  tfis  7852  nqereu  10915  rpnnen1lem2  13002  rpnnen1lem1  13003  rpnnen1lem3  13004  rpnnen1lem5  13006  qustgpopn  24258  nbusgrf1o0  29700  finsumvtxdg2ssteplem3  29878  frgrwopreglem2  30645  frgrwopreglem5lem  30652  partfun2  33002  resf1o  33056  elrgspnlem4  33546  nsgqusf1olem2  33704  nsgqusf1olem3  33705  ballotlem2  34860  reprsuc  34983  oddprm2  35023  hgt750lemb  35024  bnj1476  35216  bnj1533  35221  bnj1538  35224  bnj1523  35440  cvmlift2lem12  35787  neibastop2lem  36852  topdifinfindis  37973  topdifinffinlem  37974  stoweidlem24  46721  stoweidlem31  46728  stoweidlem52  46749  stoweidlem54  46751  stoweidlem57  46754  salexct  47031  ovolval5lem3  47351  pimdecfgtioc  47412  pimincfltioc  47413  pimdecfgtioo  47414  pimincfltioo  47415  smfsuplem1  47508  smfsuplem3  47510  smfliminflem  47527  prprsprreu  48251