Theorem reqabi 3432

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

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

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 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409

This theorem is referenced by:  fvmptss  6983  tfis  7834  nqereu  10889  rpnnen1lem2  12943  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem5  12947  qustgpopn  24014  nbusgrf1o0  29303  finsumvtxdg2ssteplem3  29482  frgrwopreglem2  30249  frgrwopreglem5lem  30256  resf1o  32660  elrgspnlem4  33203  nsgqusf1olem2  33392  nsgqusf1olem3  33393  ballotlem2  34487  reprsuc  34613  oddprm2  34653  hgt750lemb  34654  bnj1476  34844  bnj1533  34849  bnj1538  34852  bnj1523  35068  cvmlift2lem12  35308  neibastop2lem  36355  topdifinfindis  37341  topdifinffinlem  37342  stoweidlem24  46029  stoweidlem31  46036  stoweidlem52  46057  stoweidlem54  46059  stoweidlem57  46062  salexct  46339  ovolval5lem3  46659  pimdecfgtioc  46720  pimincfltioc  46721  pimdecfgtioo  46722  pimincfltioo  46723  smfsuplem1  46816  smfsuplem3  46818  smfliminflem  46835  prprsprreu  47524