Theorem elrab2 2963

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ wcel 2200  {crab 2512

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-v 2802

This theorem is referenced by:  elrabsf  3068  pwnss  4247  regexmidlemm  4628  regexmidlem1  4629  reg2exmidlema  4630  tfis  4679  ctssdccl  7301  nninff  7312  nninfninc  7313  infnninf  7314  infnninfOLD  7315  nnnninf  7316  nnnninfeq  7318  nnnninfeq2  7319  nninfwlpoimlemg  7365  exmidaclem  7413  ltexprlemell  7808  ltexprlemelu  7809  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemopu  7858  cauappcvgprlemupu  7859  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem2  7870  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemopu  7881  caucvgprlemupu  7882  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemladdfu  7887  caucvgprlem2  7890  caucvgprprlemell  7895  caucvgprprlemelu  7896  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemexbt  7916  caucvgprprlem2  7920  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  axpre-suploclemres  8111  elz  9471  elrp  9880  repos  10195  zsupssdc  10488  bitsfzolem  12505  isprm  12671  oddpwdc  12736  sqpweven  12737  2sqpwodd  12738  phimullem  12787  eulerthlem1  12789  eulerthlemfi  12790  eulerthlemrprm  12791  eulerthlemth  12794  hashgcdlem  12800  pclem0  12849  pclemub  12850  pclemdc  12851  pcprecl  12852  pcprendvds  12853  1arith  12930  elgz  12934  4sqlem13m  12966  4sqlem17  12970  4sqlem18  12971  ctiunctlemu1st  13045  ctiunctlemu2nd  13046  ctiunctlemudc  13048  ctiunctlemfo  13050  infpn2  13067  issgrp  13476  ismnddef  13491  gsumvallem2  13566  isgrp  13579  elnmz  13785  iscmn  13870  isrng  13937  issrg  13968  isring  14003  iscrng  14006  isnzr  14185  islring  14196  isrrg  14267  isdomn  14273  islmod  14295  psrbag  14673  psr1clfi  14692  isxms  15165  isms  15167  ivthinclemlm  15348  ivthinclemum  15349  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemdisj  15354  ivthinclemloc  15355  mpodvdsmulf1o  15704  lgslem2  15720  lgslem3  15721  lgsfcl2  15725  lfgredg2dom  15971  uspgredg2vlem  16059  uspgredg2v  16060  usgredg2vlem1  16061  usgredg2vlem2  16062  ushgredgedg  16065  ushgredgedgloop  16067  isclwwlknon  16225  s2elclwwlknon2  16231  0nninf  16542  nnsf  16543  peano4nninf  16544  nninfalllem1  16546  nninfself  16551  qdencn  16567