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  7310  nninff  7321  nninfninc  7322  infnninf  7323  infnninfOLD  7324  nnnninf  7325  nnnninfeq  7327  nnnninfeq2  7328  nninfwlpoimlemg  7374  exmidaclem  7423  ltexprlemell  7818  ltexprlemelu  7819  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem2  7880  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprlem2  7900  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemexbt  7926  caucvgprprlem2  7930  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  axpre-suploclemres  8121  elz  9481  elrp  9890  repos  10205  zsupssdc  10499  bitsfzolem  12520  isprm  12686  oddpwdc  12751  sqpweven  12752  2sqpwodd  12753  phimullem  12802  eulerthlem1  12804  eulerthlemfi  12805  eulerthlemrprm  12806  eulerthlemth  12809  hashgcdlem  12815  pclem0  12864  pclemub  12865  pclemdc  12866  pcprecl  12867  pcprendvds  12868  1arith  12945  elgz  12949  4sqlem13m  12981  4sqlem17  12985  4sqlem18  12986  ctiunctlemu1st  13060  ctiunctlemu2nd  13061  ctiunctlemudc  13063  ctiunctlemfo  13065  infpn2  13082  issgrp  13491  ismnddef  13506  gsumvallem2  13581  isgrp  13594  elnmz  13800  iscmn  13885  isrng  13953  issrg  13984  isring  14019  iscrng  14022  isnzr  14201  islring  14212  isrrg  14283  isdomn  14289  islmod  14311  psrbag  14689  psr1clfi  14708  isxms  15181  isms  15183  ivthinclemlm  15364  ivthinclemum  15365  ivthinclemlopn  15366  ivthinclemlr  15367  ivthinclemuopn  15368  ivthinclemur  15369  ivthinclemdisj  15370  ivthinclemloc  15371  mpodvdsmulf1o  15720  lgslem2  15736  lgslem3  15737  lgsfcl2  15741  lfgredg2dom  15989  uspgredg2vlem  16077  uspgredg2v  16078  usgredg2vlem1  16079  usgredg2vlem2  16080  ushgredgedg  16083  ushgredgedgloop  16085  isclwwlknon  16287  s2elclwwlknon2  16293  0nninf  16632  nnsf  16633  peano4nninf  16634  nninfalllem1  16636  nninfself  16641  qdencn  16657