Theorem reqabi 3438

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417

This theorem is used by:  fvmptss  7032  tfis  7893  nqereu  11044  rpnnen1lem2  13135  rpnnen1lem1  13136  rpnnen1lem3  13137  rpnnen1lem5  13139  qustgpopn  24472  nbusgrf1o0  29983  finsumvtxdg2ssteplem3  30161  frgrwopreglem2  30947  frgrwopreglem5lem  30954  partfun2  33344  resf1o  33395  elrgspnlem4  33882  nsgqusf1olem2  34049  nsgqusf1olem3  34050  ballotlem2  35204  reprsuc  35327  oddprm2  35367  hgt750lemb  35368  bnj1476  35560  bnj1533  35565  bnj1538  35568  bnj1523  35784  cvmlift2lem12  36259  neibastop2lem  37339  topdifinfindis  38474  topdifinffinlem  38475  stoweidlem24  47249  stoweidlem31  47256  stoweidlem52  47277  stoweidlem54  47279  stoweidlem57  47282  salexct  47559  ovolval5lem3  47879  pimdecfgtioc  47940  pimincfltioc  47941  pimdecfgtioo  47942  pimincfltioo  47943  smfsuplem1  48036  smfsuplem3  48038  smfliminflem  48055  prprsprreu  48816