Theorem reqabi 3460

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437

This theorem is referenced by:  fvmptss  7028  tfis  7876  nqereu  10969  rpnnen1lem2  13019  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  qustgpopn  24128  addsproplem2  28003  sleadd1  28022  negsproplem6  28065  negsid  28073  nbusgrf1o0  29386  finsumvtxdg2ssteplem3  29565  frgrwopreglem2  30332  frgrwopreglem5lem  30339  resf1o  32741  elrgspnlem4  33249  nsgqusf1olem2  33442  nsgqusf1olem3  33443  ballotlem2  34491  reprsuc  34630  oddprm2  34670  hgt750lemb  34671  bnj1476  34861  bnj1533  34866  bnj1538  34869  bnj1523  35085  cvmlift2lem12  35319  neibastop2lem  36361  topdifinfindis  37347  topdifinffinlem  37348  stoweidlem24  46039  stoweidlem31  46046  stoweidlem52  46067  stoweidlem54  46069  stoweidlem57  46072  salexct  46349  ovolval5lem3  46669  pimdecfgtioc  46730  pimincfltioc  46731  pimdecfgtioo  46732  pimincfltioo  46733  smfsuplem1  46826  smfsuplem3  46828  smfliminflem  46845  prprsprreu  47506