Theorem reqabi 3435

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

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

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 2147  ax-9 2155  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414

This theorem is used by:  fvmptss  6998  tfis  7855  nqereu  10995  rpnnen1lem2  13086  rpnnen1lem1  13087  rpnnen1lem3  13088  rpnnen1lem5  13090  qustgpopn  24419  nbusgrf1o0  29932  finsumvtxdg2ssteplem3  30110  frgrwopreglem2  30896  frgrwopreglem5lem  30903  partfun2  33252  resf1o  33304  elrgspnlem4  33788  nsgqusf1olem2  33947  nsgqusf1olem3  33948  ballotlem2  35104  reprsuc  35227  oddprm2  35267  hgt750lemb  35268  bnj1476  35460  bnj1533  35465  bnj1538  35468  bnj1523  35684  cvmlift2lem12  36048  neibastop2lem  37118  topdifinfindis  38237  topdifinffinlem  38238  stoweidlem24  46978  stoweidlem31  46985  stoweidlem52  47006  stoweidlem54  47008  stoweidlem57  47011  salexct  47288  ovolval5lem3  47608  pimdecfgtioc  47669  pimincfltioc  47670  pimdecfgtioo  47671  pimincfltioo  47672  smfsuplem1  47765  smfsuplem3  47767  smfliminflem  47784  prprsprreu  48545