Theorem rabeq2i 3488

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

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  {crab 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147

This theorem is referenced by:  fvmptss  6775  tfis  7563  nqereu  10345  rpnnen1lem2  12370  rpnnen1lem1  12371  rpnnen1lem3  12372  rpnnen1lem5  12374  qustgpopn  22722  nbusgrf1o0  27145  finsumvtxdg2ssteplem3  27323  frgrwopreglem2  28086  frgrwopreglem5lem  28093  resf1o  30460  ballotlem2  31741  reprsuc  31881  oddprm2  31921  hgt750lemb  31922  bnj1476  32114  bnj1533  32119  bnj1538  32122  bnj1523  32338  cvmlift2lem12  32556  neibastop2lem  33703  topdifinfindis  34621  topdifinffinlem  34622  stoweidlem24  42302  stoweidlem31  42309  stoweidlem52  42330  stoweidlem54  42332  stoweidlem57  42335  salexct  42610  ovolval5lem3  42929  pimdecfgtioc  42986  pimincfltioc  42987  pimdecfgtioo  42988  pimincfltioo  42989  smfsuplem1  43078  smfsuplem3  43080  smfliminflem  43097  prprsprreu  43674