Theorem reqabi 3413

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

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

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 3391

This theorem is referenced by:  fvmptss  6952  tfis  7797  nqereu  10841  rpnnen1lem2  12891  rpnnen1lem1  12892  rpnnen1lem3  12893  rpnnen1lem5  12895  qustgpopn  24063  nbusgrf1o0  29426  finsumvtxdg2ssteplem3  29605  frgrwopreglem2  30372  frgrwopreglem5lem  30379  partfun2  32738  resf1o  32792  elrgspnlem4  33311  nsgqusf1olem2  33479  nsgqusf1olem3  33480  ballotlem2  34639  reprsuc  34765  oddprm2  34805  hgt750lemb  34806  bnj1476  34995  bnj1533  35000  bnj1538  35003  bnj1523  35219  cvmlift2lem12  35502  neibastop2lem  36548  topdifinfindis  37658  topdifinffinlem  37659  stoweidlem24  46456  stoweidlem31  46463  stoweidlem52  46484  stoweidlem54  46486  stoweidlem57  46489  salexct  46766  ovolval5lem3  47086  pimdecfgtioc  47147  pimincfltioc  47148  pimdecfgtioo  47149  pimincfltioo  47150  smfsuplem1  47243  smfsuplem3  47245  smfliminflem  47262  prprsprreu  47953