Theorem reqabi 3424

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {crab 3401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402

This theorem is referenced by:  fvmptss  6962  tfis  7807  nqereu  10852  rpnnen1lem2  12902  rpnnen1lem1  12903  rpnnen1lem3  12904  rpnnen1lem5  12906  qustgpopn  24076  nbusgrf1o0  29454  finsumvtxdg2ssteplem3  29633  frgrwopreglem2  30400  frgrwopreglem5lem  30407  partfun2  32765  resf1o  32819  elrgspnlem4  33338  nsgqusf1olem2  33506  nsgqusf1olem3  33507  ballotlem2  34666  reprsuc  34792  oddprm2  34832  hgt750lemb  34833  bnj1476  35022  bnj1533  35027  bnj1538  35030  bnj1523  35246  cvmlift2lem12  35527  neibastop2lem  36573  topdifinfindis  37595  topdifinffinlem  37596  stoweidlem24  46376  stoweidlem31  46383  stoweidlem52  46404  stoweidlem54  46406  stoweidlem57  46409  salexct  46686  ovolval5lem3  47006  pimdecfgtioc  47067  pimincfltioc  47068  pimdecfgtioo  47069  pimincfltioo  47070  smfsuplem1  47163  smfsuplem3  47165  smfliminflem  47182  prprsprreu  47873