Theorem reqabi 3437

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415

This theorem is used by:  fvmptss  7003  tfis  7855  nqereu  10942  rpnnen1lem2  13031  rpnnen1lem1  13032  rpnnen1lem3  13033  rpnnen1lem5  13035  qustgpopn  24352  nbusgrf1o0  29837  finsumvtxdg2ssteplem3  30015  frgrwopreglem2  30801  frgrwopreglem5lem  30808  partfun2  33157  resf1o  33209  elrgspnlem4  33693  nsgqusf1olem2  33851  nsgqusf1olem3  33852  ballotlem2  35008  reprsuc  35131  oddprm2  35171  hgt750lemb  35172  bnj1476  35364  bnj1533  35369  bnj1538  35372  bnj1523  35588  cvmlift2lem12  35901  neibastop2lem  36987  topdifinfindis  38108  topdifinffinlem  38109  stoweidlem24  46860  stoweidlem31  46867  stoweidlem52  46888  stoweidlem54  46890  stoweidlem57  46893  salexct  47170  ovolval5lem3  47490  pimdecfgtioc  47551  pimincfltioc  47552  pimdecfgtioo  47553  pimincfltioo  47554  smfsuplem1  47647  smfsuplem3  47649  smfliminflem  47666  prprsprreu  48427