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  7007  tfis  7867  nqereu  11018  rpnnen1lem2  13109  rpnnen1lem1  13110  rpnnen1lem3  13111  rpnnen1lem5  13113  qustgpopn  24445  nbusgrf1o0  29956  finsumvtxdg2ssteplem3  30134  frgrwopreglem2  30920  frgrwopreglem5lem  30927  partfun2  33318  resf1o  33369  elrgspnlem4  33853  nsgqusf1olem2  34012  nsgqusf1olem3  34013  ballotlem2  35168  reprsuc  35291  oddprm2  35331  hgt750lemb  35332  bnj1476  35524  bnj1533  35529  bnj1538  35532  bnj1523  35748  cvmlift2lem12  36166  neibastop2lem  37241  topdifinfindis  38363  topdifinffinlem  38364  stoweidlem24  47128  stoweidlem31  47135  stoweidlem52  47156  stoweidlem54  47158  stoweidlem57  47161  salexct  47438  ovolval5lem3  47758  pimdecfgtioc  47819  pimincfltioc  47820  pimdecfgtioo  47821  pimincfltioo  47822  smfsuplem1  47915  smfsuplem3  47917  smfliminflem  47934  prprsprreu  48695