Theorem rabeq2i 3435

Description: Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.)

Hypothesis

Ref	Expression
rabeq2i.1	⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑}

Assertion

Ref	Expression
rabeq2i	⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))

Proof of Theorem rabeq2i

Step	Hyp	Ref	Expression
1		rabeq2i.1	. . 3 ⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑}
2	1	eleq2i 2876	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑})
3		rabid 3339	. 2 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	2, 3	bitri 276	1 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1525   ∈ wcel 2083  {crab 3111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1528  df-ex 1766  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-rab 3116

This theorem is referenced by:  fvmptss  6653  tfis  7432  nqereu  10204  rpnnen1lem2  12230  rpnnen1lem1  12231  rpnnen1lem3  12232  rpnnen1lem5  12234  qustgpopn  22415  nbusgrf1o0  26838  finsumvtxdg2ssteplem3  27016  frgrwopreglem2  27780  frgrwopreglem5lem  27787  resf1o  30150  ballotlem2  31359  reprsuc  31499  oddprm2  31539  hgt750lemb  31540  bnj1476  31731  bnj1533  31736  bnj1538  31739  bnj1523  31953  cvmlift2lem12  32171  neibastop2lem  33319  topdifinfindis  34179  topdifinffinlem  34180  stoweidlem24  41873  stoweidlem31  41880  stoweidlem52  41901  stoweidlem54  41903  stoweidlem57  41906  salexct  42181  ovolval5lem3  42500  pimdecfgtioc  42557  pimincfltioc  42558  pimdecfgtioo  42559  pimincfltioo  42560  smfsuplem1  42649  smfsuplem3  42651  smfliminflem  42668  prprsprreu  43185