Theorem reqabi 3453

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

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1540   ∈ wcel 2105  {crab 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-12 2170  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432

This theorem is referenced by:  fvmptss  7010  tfis  7848  nqereu  10930  rpnnen1lem2  12968  rpnnen1lem1  12969  rpnnen1lem3  12970  rpnnen1lem5  12972  qustgpopn  23945  addsproplem2  27802  sleadd1  27821  negsproplem6  27860  negsid  27868  nbusgrf1o0  29061  finsumvtxdg2ssteplem3  29239  frgrwopreglem2  30001  frgrwopreglem5lem  30008  resf1o  32390  nsgqusf1olem2  32967  nsgqusf1olem3  32968  ballotlem2  33953  reprsuc  34093  oddprm2  34133  hgt750lemb  34134  bnj1476  34324  bnj1533  34329  bnj1538  34332  bnj1523  34548  cvmlift2lem12  34771  neibastop2lem  35712  topdifinfindis  36694  topdifinffinlem  36695  stoweidlem24  45202  stoweidlem31  45209  stoweidlem52  45230  stoweidlem54  45232  stoweidlem57  45235  salexct  45512  ovolval5lem3  45832  pimdecfgtioc  45893  pimincfltioc  45894  pimdecfgtioo  45895  pimincfltioo  45896  smfsuplem1  45989  smfsuplem3  45991  smfliminflem  46008  prprsprreu  46649