Theorem reqabi 3422

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {crab 3399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400

This theorem is referenced by:  fvmptss  6953  tfis  7797  nqereu  10840  rpnnen1lem2  12890  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem5  12894  qustgpopn  24064  nbusgrf1o0  29442  finsumvtxdg2ssteplem3  29621  frgrwopreglem2  30388  frgrwopreglem5lem  30395  partfun2  32755  resf1o  32809  elrgspnlem4  33327  nsgqusf1olem2  33495  nsgqusf1olem3  33496  ballotlem2  34646  reprsuc  34772  oddprm2  34812  hgt750lemb  34813  bnj1476  35003  bnj1533  35008  bnj1538  35011  bnj1523  35227  cvmlift2lem12  35508  neibastop2lem  36554  topdifinfindis  37547  topdifinffinlem  37548  stoweidlem24  46264  stoweidlem31  46271  stoweidlem52  46292  stoweidlem54  46294  stoweidlem57  46297  salexct  46574  ovolval5lem3  46894  pimdecfgtioc  46955  pimincfltioc  46956  pimdecfgtioo  46957  pimincfltioo  46958  smfsuplem1  47051  smfsuplem3  47053  smfliminflem  47070  prprsprreu  47761