Theorem reqabi 3413

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {crab 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391

This theorem is referenced by:  fvmptss  6954  tfis  7799  nqereu  10843  rpnnen1lem2  12918  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem5  12922  qustgpopn  24095  nbusgrf1o0  29452  finsumvtxdg2ssteplem3  29631  frgrwopreglem2  30398  frgrwopreglem5lem  30405  partfun2  32764  resf1o  32818  elrgspnlem4  33321  nsgqusf1olem2  33489  nsgqusf1olem3  33490  ballotlem2  34649  reprsuc  34775  oddprm2  34815  hgt750lemb  34816  bnj1476  35005  bnj1533  35010  bnj1538  35013  bnj1523  35229  cvmlift2lem12  35512  neibastop2lem  36558  topdifinfindis  37676  topdifinffinlem  37677  stoweidlem24  46470  stoweidlem31  46477  stoweidlem52  46498  stoweidlem54  46500  stoweidlem57  46503  salexct  46780  ovolval5lem3  47100  pimdecfgtioc  47161  pimincfltioc  47162  pimdecfgtioo  47163  pimincfltioo  47164  smfsuplem1  47257  smfsuplem3  47259  smfliminflem  47276  prprsprreu  47991