Theorem elrab2 2965

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 2298	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑})
3		elrab2.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elrab 2962	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
5	2, 4	bitri 184	1 ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1397   ∈ wcel 2202  {crab 2514

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-v 2804

This theorem is referenced by:  elrabsf  3070  pwnss  4249  regexmidlemm  4630  regexmidlem1  4631  reg2exmidlema  4632  tfis  4681  ctssdccl  7309  nninff  7320  nninfninc  7321  infnninf  7322  infnninfOLD  7323  nnnninf  7324  nnnninfeq  7326  nnnninfeq2  7327  nninfwlpoimlemg  7373  exmidaclem  7422  ltexprlemell  7817  ltexprlemelu  7818  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemopu  7867  cauappcvgprlemupu  7868  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem2  7879  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemopu  7890  caucvgprlemupu  7891  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemladdfu  7896  caucvgprlem2  7899  caucvgprprlemell  7904  caucvgprprlemelu  7905  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemexbt  7925  caucvgprprlem2  7929  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  axpre-suploclemres  8120  elz  9480  elrp  9889  repos  10204  zsupssdc  10497  bitsfzolem  12514  isprm  12680  oddpwdc  12745  sqpweven  12746  2sqpwodd  12747  phimullem  12796  eulerthlem1  12798  eulerthlemfi  12799  eulerthlemrprm  12800  eulerthlemth  12803  hashgcdlem  12809  pclem0  12858  pclemub  12859  pclemdc  12860  pcprecl  12861  pcprendvds  12862  1arith  12939  elgz  12943  4sqlem13m  12975  4sqlem17  12979  4sqlem18  12980  ctiunctlemu1st  13054  ctiunctlemu2nd  13055  ctiunctlemudc  13057  ctiunctlemfo  13059  infpn2  13076  issgrp  13485  ismnddef  13500  gsumvallem2  13575  isgrp  13588  elnmz  13794  iscmn  13879  isrng  13946  issrg  13977  isring  14012  iscrng  14015  isnzr  14194  islring  14205  isrrg  14276  isdomn  14282  islmod  14304  psrbag  14682  psr1clfi  14701  isxms  15174  isms  15176  ivthinclemlm  15357  ivthinclemum  15358  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemdisj  15363  ivthinclemloc  15364  mpodvdsmulf1o  15713  lgslem2  15729  lgslem3  15730  lgsfcl2  15734  lfgredg2dom  15982  uspgredg2vlem  16070  uspgredg2v  16071  usgredg2vlem1  16072  usgredg2vlem2  16073  ushgredgedg  16076  ushgredgedgloop  16078  isclwwlknon  16280  s2elclwwlknon2  16286  0nninf  16606  nnsf  16607  peano4nninf  16608  nninfalllem1  16610  nninfself  16615  qdencn  16631