Theorem rabeq2i 3197

Description: Inference rule 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 2693	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑})
3		rabid 3116	. 2 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))
4	2, 3	bitri 264	1 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))

Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990  {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-rab 2921

This theorem is referenced by:  fvmptss  6292  tfis  7054  nqereu  9751  rpnnen1lem2  11814  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  qustgpopn  21923  nbusgrf1o0  26271  finsumvtxdg2ssteplem3  26443  clwlksfclwwlk2wrd  26958  clwlksfclwwlk1hash  26960  clwlksfclwwlk  26962  frgrwopreglem2  27177  frgrwopreglem5lem  27184  resf1o  29505  ballotlem2  30550  reprsuc  30693  oddprm2  30733  hgt750lemb  30734  bnj1476  30917  bnj1533  30922  bnj1538  30925  bnj1523  31139  cvmlift2lem12  31296  neibastop2lem  32355  topdifinfindis  33194  topdifinffinlem  33195  stoweidlem24  40241  stoweidlem31  40248  stoweidlem52  40269  stoweidlem54  40271  stoweidlem57  40274  salexct  40552  ovolval5lem3  40868  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  smfsuplem1  41017  smfsuplem3  41019  smfliminflem  41036