Theorem reqabi 3457

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2106  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434

This theorem is referenced by:  fvmptss  7028  tfis  7876  nqereu  10967  rpnnen1lem2  13017  rpnnen1lem1  13018  rpnnen1lem3  13019  rpnnen1lem5  13021  qustgpopn  24144  addsproplem2  28018  sleadd1  28037  negsproplem6  28080  negsid  28088  nbusgrf1o0  29401  finsumvtxdg2ssteplem3  29580  frgrwopreglem2  30342  frgrwopreglem5lem  30349  resf1o  32748  elrgspnlem4  33235  nsgqusf1olem2  33422  nsgqusf1olem3  33423  ballotlem2  34470  reprsuc  34609  oddprm2  34649  hgt750lemb  34650  bnj1476  34840  bnj1533  34845  bnj1538  34848  bnj1523  35064  cvmlift2lem12  35299  neibastop2lem  36343  topdifinfindis  37329  topdifinffinlem  37330  stoweidlem24  45980  stoweidlem31  45987  stoweidlem52  46008  stoweidlem54  46010  stoweidlem57  46013  salexct  46290  ovolval5lem3  46610  pimdecfgtioc  46671  pimincfltioc  46672  pimdecfgtioo  46673  pimincfltioo  46674  smfsuplem1  46767  smfsuplem3  46769  smfliminflem  46786  prprsprreu  47444