Theorem reqabi 3467

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444

This theorem is referenced by:  fvmptss  7041  tfis  7892  nqereu  10998  rpnnen1lem2  13042  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem5  13046  qustgpopn  24149  addsproplem2  28021  sleadd1  28040  negsproplem6  28083  negsid  28091  nbusgrf1o0  29404  finsumvtxdg2ssteplem3  29583  frgrwopreglem2  30345  frgrwopreglem5lem  30352  resf1o  32744  nsgqusf1olem2  33407  nsgqusf1olem3  33408  ballotlem2  34453  reprsuc  34592  oddprm2  34632  hgt750lemb  34633  bnj1476  34823  bnj1533  34828  bnj1538  34831  bnj1523  35047  cvmlift2lem12  35282  neibastop2lem  36326  topdifinfindis  37312  topdifinffinlem  37313  stoweidlem24  45945  stoweidlem31  45952  stoweidlem52  45973  stoweidlem54  45975  stoweidlem57  45978  salexct  46255  ovolval5lem3  46575  pimdecfgtioc  46636  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  smfsuplem1  46732  smfsuplem3  46734  smfliminflem  46751  prprsprreu  47393