Theorem reqabi 3439

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

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

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 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416

This theorem is referenced by:  fvmptss  6998  tfis  7850  nqereu  10943  rpnnen1lem2  12993  rpnnen1lem1  12994  rpnnen1lem3  12995  rpnnen1lem5  12997  qustgpopn  24058  nbusgrf1o0  29348  finsumvtxdg2ssteplem3  29527  frgrwopreglem2  30294  frgrwopreglem5lem  30301  resf1o  32707  elrgspnlem4  33240  nsgqusf1olem2  33429  nsgqusf1olem3  33430  ballotlem2  34521  reprsuc  34647  oddprm2  34687  hgt750lemb  34688  bnj1476  34878  bnj1533  34883  bnj1538  34886  bnj1523  35102  cvmlift2lem12  35336  neibastop2lem  36378  topdifinfindis  37364  topdifinffinlem  37365  stoweidlem24  46053  stoweidlem31  46060  stoweidlem52  46081  stoweidlem54  46083  stoweidlem57  46086  salexct  46363  ovolval5lem3  46683  pimdecfgtioc  46744  pimincfltioc  46745  pimdecfgtioo  46746  pimincfltioo  46747  smfsuplem1  46840  smfsuplem3  46842  smfliminflem  46859  prprsprreu  47533