Theorem rabeq2i 3170

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

Syntax hints:   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {crab 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-rab 2905

This theorem is referenced by:  fvmptss  6201  tfis  6946  nqereu  9630  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  qustgpopn  21733  clwlkfclwwlk2wrd  26367  clwlkfclwwlk1hash  26369  clwlkfclwwlk  26371  frgrawopreglem2  26572  frgrawopreg  26576  resf1o  28893  ballotlem2  29877  bnj1476  30171  bnj1533  30176  bnj1538  30179  bnj1523  30393  cvmlift2lem12  30550  neibastop2lem  31525  topdifinfindis  32370  topdifinffinlem  32371  stoweidlem24  38917  stoweidlem31  38924  stoweidlem52  38945  stoweidlem54  38947  stoweidlem57  38950  salexct  39228  nbusgrf1o0  40597  clwlksfclwwlk2wrd  41265  clwlksfclwwlk1hash  41267  clwlksfclwwlk  41269  frgrwopreglem2  41482  frgrwopreg  41486