Theorem reqabi 3419

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397

This theorem is referenced by:  fvmptss  6947  tfis  7791  nqereu  10827  rpnnen1lem2  12877  rpnnen1lem1  12878  rpnnen1lem3  12879  rpnnen1lem5  12881  qustgpopn  24036  nbusgrf1o0  29349  finsumvtxdg2ssteplem3  29528  frgrwopreglem2  30295  frgrwopreglem5lem  30302  partfun2  32661  resf1o  32717  elrgspnlem4  33219  nsgqusf1olem2  33386  nsgqusf1olem3  33387  ballotlem2  34523  reprsuc  34649  oddprm2  34689  hgt750lemb  34690  bnj1476  34880  bnj1533  34885  bnj1538  34888  bnj1523  35104  cvmlift2lem12  35379  neibastop2lem  36425  topdifinfindis  37411  topdifinffinlem  37412  stoweidlem24  46146  stoweidlem31  46153  stoweidlem52  46174  stoweidlem54  46176  stoweidlem57  46179  salexct  46456  ovolval5lem3  46776  pimdecfgtioc  46837  pimincfltioc  46838  pimdecfgtioo  46839  pimincfltioo  46840  smfsuplem1  46933  smfsuplem3  46935  smfliminflem  46952  prprsprreu  47643