Theorem elrab2 2923

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.)

Hypotheses

Ref	Expression
elrab2.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
elrab2.2	⊢ 𝐶 = {𝑥 ∈ 𝐵 ∣ 𝜑}

Assertion

Ref	Expression
elrab2	⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)

Proof of Theorem elrab2

Step	Hyp	Ref	Expression
1		elrab2.2	. . 3 ⊢ 𝐶 = {𝑥 ∈ 𝐵 ∣ 𝜑}
2	1	eleq2i 2263	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑})
3		elrab2.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elrab 2920	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
5	2, 4	bitri 184	1 ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1364   ∈ wcel 2167  {crab 2479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rab 2484  df-v 2765

This theorem is referenced by:  elrabsf  3028  pwnss  4193  regexmidlemm  4569  regexmidlem1  4570  reg2exmidlema  4571  tfis  4620  ctssdccl  7186  nninff  7197  nninfninc  7198  infnninf  7199  infnninfOLD  7200  nnnninf  7201  nnnninfeq  7203  nnnninfeq2  7204  nninfwlpoimlemg  7250  exmidaclem  7293  ltexprlemell  7684  ltexprlemelu  7685  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemopu  7734  cauappcvgprlemupu  7735  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  cauappcvgprlem2  7746  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemopu  7757  caucvgprlemupu  7758  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemladdfu  7763  caucvgprlem2  7766  caucvgprprlemell  7771  caucvgprprlemelu  7772  caucvgprprlemml  7780  caucvgprprlemmu  7781  caucvgprprlemexbt  7792  caucvgprprlem2  7796  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  axpre-suploclemres  7987  elz  9347  elrp  9749  repos  10064  zsupssdc  10347  bitsfzolem  12138  isprm  12304  oddpwdc  12369  sqpweven  12370  2sqpwodd  12371  phimullem  12420  eulerthlem1  12422  eulerthlemfi  12423  eulerthlemrprm  12424  eulerthlemth  12427  hashgcdlem  12433  pclem0  12482  pclemub  12483  pclemdc  12484  pcprecl  12485  pcprendvds  12486  1arith  12563  elgz  12567  4sqlem13m  12599  4sqlem17  12603  4sqlem18  12604  ctiunctlemu1st  12678  ctiunctlemu2nd  12679  ctiunctlemudc  12681  ctiunctlemfo  12683  infpn2  12700  issgrp  13107  ismnddef  13122  gsumvallem2  13197  isgrp  13210  elnmz  13416  iscmn  13501  isrng  13568  issrg  13599  isring  13634  iscrng  13637  isnzr  13815  islring  13826  isrrg  13897  isdomn  13903  islmod  13925  psrbag  14303  psr1clfi  14322  isxms  14795  isms  14797  ivthinclemlm  14978  ivthinclemum  14979  ivthinclemlopn  14980  ivthinclemlr  14981  ivthinclemuopn  14982  ivthinclemur  14983  ivthinclemdisj  14984  ivthinclemloc  14985  mpodvdsmulf1o  15334  lgslem2  15350  lgslem3  15351  lgsfcl2  15355  0nninf  15759  nnsf  15760  peano4nninf  15761  nninfalllem1  15763  nninfself  15768  qdencn  15784