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  23944  addsproplem2  27800  sleadd1  27819  negsproplem6  27858  negsid  27866  nbusgrf1o0  29059  finsumvtxdg2ssteplem3  29237  frgrwopreglem2  29999  frgrwopreglem5lem  30006  resf1o  32388  nsgqusf1olem2  32965  nsgqusf1olem3  32966  ballotlem2  33951  reprsuc  34091  oddprm2  34131  hgt750lemb  34132  bnj1476  34322  bnj1533  34327  bnj1538  34330  bnj1523  34546  cvmlift2lem12  34769  neibastop2lem  35709  topdifinfindis  36691  topdifinffinlem  36692  stoweidlem24  45199  stoweidlem31  45206  stoweidlem52  45227  stoweidlem54  45229  stoweidlem57  45232  salexct  45509  ovolval5lem3  45829  pimdecfgtioc  45890  pimincfltioc  45891  pimdecfgtioo  45892  pimincfltioo  45893  smfsuplem1  45986  smfsuplem3  45988  smfliminflem  46005  prprsprreu  46646