Theorem reqabi 3442

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  {crab 3419

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-12 2216  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420

This theorem is used by:  fvmptss  7009  tfis  7860  nqereu  10932  rpnnen1lem2  13019  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  qustgpopn  24314  nbusgrf1o0  29756  finsumvtxdg2ssteplem3  29934  frgrwopreglem2  30701  frgrwopreglem5lem  30708  partfun2  33058  resf1o  33112  elrgspnlem4  33596  nsgqusf1olem2  33754  nsgqusf1olem3  33755  ballotlem2  34911  reprsuc  35034  oddprm2  35074  hgt750lemb  35075  bnj1476  35267  bnj1533  35272  bnj1538  35275  bnj1523  35491  cvmlift2lem12  35827  neibastop2lem  36912  topdifinfindis  38033  topdifinffinlem  38034  stoweidlem24  46779  stoweidlem31  46786  stoweidlem52  46807  stoweidlem54  46809  stoweidlem57  46812  salexct  47089  ovolval5lem3  47409  pimdecfgtioc  47470  pimincfltioc  47471  pimdecfgtioo  47472  pimincfltioo  47473  smfsuplem1  47566  smfsuplem3  47568  smfliminflem  47585  prprsprreu  48309