Theorem reqabi 3434

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413

This theorem is used by:  fvmptss  7006  tfis  7866  nqereu  11014  rpnnen1lem2  13105  rpnnen1lem1  13106  rpnnen1lem3  13107  rpnnen1lem5  13109  qustgpopn  24439  nbusgrf1o0  29950  finsumvtxdg2ssteplem3  30128  frgrwopreglem2  30914  frgrwopreglem5lem  30921  partfun2  33270  resf1o  33322  elrgspnlem4  33806  nsgqusf1olem2  33965  nsgqusf1olem3  33966  ballotlem2  35121  reprsuc  35244  oddprm2  35284  hgt750lemb  35285  bnj1476  35477  bnj1533  35482  bnj1538  35485  bnj1523  35701  cvmlift2lem12  36079  neibastop2lem  37148  topdifinfindis  38270  topdifinffinlem  38271  stoweidlem24  47034  stoweidlem31  47041  stoweidlem52  47062  stoweidlem54  47064  stoweidlem57  47067  salexct  47344  ovolval5lem3  47664  pimdecfgtioc  47725  pimincfltioc  47726  pimdecfgtioo  47727  pimincfltioo  47728  smfsuplem1  47821  smfsuplem3  47823  smfliminflem  47840  prprsprreu  48601