Theorem elrab2 2979

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1398   ∈ wcel 2205  {crab 2526

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rab 2531  df-v 2817

This theorem is referenced by:  elrabsf  3084  pwnss  4277  regexmidlemm  4659  regexmidlem1  4660  reg2exmidlema  4661  tfis  4710  ctssdccl  7415  nninff  7426  nninfninc  7427  infnninf  7428  infnninfOLD  7429  nnnninf  7430  nnnninfeq  7432  nnnninfeq2  7433  nninfwlpoimlemg  7479  exmidaclem  7528  ltexprlemell  7929  ltexprlemelu  7930  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem2  7991  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemladdfu  8008  caucvgprlem2  8011  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemexbt  8037  caucvgprprlem2  8041  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  axpre-suploclemres  8232  elz  9596  elrp  10006  repos  10322  zsupssdc  10622  bitsfzolem  12665  isprm  12831  oddpwdc  12896  sqpweven  12897  2sqpwodd  12898  phimullem  12947  eulerthlem1  12949  eulerthlemfi  12950  eulerthlemrprm  12951  eulerthlemth  12954  hashgcdlem  12960  pclem0  13009  pclemub  13010  pclemdc  13011  pcprecl  13012  pcprendvds  13013  1arith  13090  elgz  13094  4sqlem13m  13126  4sqlem17  13130  4sqlem18  13131  ballotfilemelo  13166  ballotfileme  13180  ballotfilemscl  13191  ctiunctlemu1st  13269  ctiunctlemu2nd  13270  ctiunctlemudc  13272  ctiunctlemfo  13274  infpn2  13291  issgrp  13666  ismnddef  13679  gsumvallem2  13748  isgrp  13761  elnmz  13961  iscmn  14046  isrng  14173  issrg  14208  isring  14243  iscrng  14246  isnzr  14426  islring  14437  isrrg  14509  isdomn  14516  isdrngtap  14544  islmod  14565  psrbag  14943  psrbagconcl  14953  psr1clfi  14969  isxms  15442  isms  15444  ivthinclemlm  15625  ivthinclemum  15626  ivthinclemlopn  15627  ivthinclemlr  15628  ivthinclemuopn  15629  ivthinclemur  15630  ivthinclemdisj  15631  ivthinclemloc  15632  mpodvdsmulf1o  15984  lgslem2  16000  lgslem3  16001  lgsfcl2  16005  lfgredg2dom  16253  uspgredg2vlem  16341  uspgredg2v  16342  usgredg2vlem1  16343  usgredg2vlem2  16344  ushgredgedg  16347  ushgredgedgloop  16349  isclwwlknon  16551  s2elclwwlknon2  16557  0nninf  16908  nnsf  16909  peano4nninf  16910  nninfalllem1  16912  nninfself  16917  qdencn  16933