Theorem reqabi 3436

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

Syntax hints:   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141  {crab 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414

This theorem is referenced by:  fvmptss  6982  tfis  7829  nqereu  10880  rpnnen1lem2  12971  rpnnen1lem1  12972  rpnnen1lem3  12973  rpnnen1lem5  12975  qustgpopn  24167  nbusgrf1o0  29526  finsumvtxdg2ssteplem3  29704  frgrwopreglem2  30471  frgrwopreglem5lem  30478  partfun2  32838  resf1o  32892  elrgspnlem4  33386  nsgqusf1olem2  33560  nsgqusf1olem3  33561  ballotlem2  34746  reprsuc  34869  oddprm2  34909  hgt750lemb  34910  bnj1476  35102  bnj1533  35107  bnj1538  35110  bnj1523  35326  cvmlift2lem12  35624  neibastop2lem  36680  topdifinfindis  37800  topdifinffinlem  37801  stoweidlem24  46558  stoweidlem31  46565  stoweidlem52  46586  stoweidlem54  46588  stoweidlem57  46591  salexct  46868  ovolval5lem3  47188  pimdecfgtioc  47249  pimincfltioc  47250  pimdecfgtioo  47251  pimincfltioo  47252  smfsuplem1  47345  smfsuplem3  47347  smfliminflem  47364  prprsprreu  48085