Theorem elrab2 2931

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1372   ∈ wcel 2175  {crab 2487

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rab 2492  df-v 2773

This theorem is referenced by:  elrabsf  3036  pwnss  4202  regexmidlemm  4578  regexmidlem1  4579  reg2exmidlema  4580  tfis  4629  ctssdccl  7195  nninff  7206  nninfninc  7207  infnninf  7208  infnninfOLD  7209  nnnninf  7210  nnnninfeq  7212  nnnninfeq2  7213  nninfwlpoimlemg  7259  exmidaclem  7302  ltexprlemell  7693  ltexprlemelu  7694  cauappcvgprlemm  7740  cauappcvgprlemopl  7741  cauappcvgprlemlol  7742  cauappcvgprlemopu  7743  cauappcvgprlemupu  7744  cauappcvgprlemdisj  7746  cauappcvgprlemloc  7747  cauappcvgprlemladdfu  7749  cauappcvgprlemladdfl  7750  cauappcvgprlemladdru  7751  cauappcvgprlemladdrl  7752  cauappcvgprlem2  7755  caucvgprlemm  7763  caucvgprlemopl  7764  caucvgprlemlol  7765  caucvgprlemopu  7766  caucvgprlemupu  7767  caucvgprlemdisj  7769  caucvgprlemloc  7770  caucvgprlemladdfu  7772  caucvgprlem2  7775  caucvgprprlemell  7780  caucvgprprlemelu  7781  caucvgprprlemml  7789  caucvgprprlemmu  7790  caucvgprprlemexbt  7801  caucvgprprlem2  7805  suplocsrlemb  7901  suplocsrlempr  7902  suplocsrlem  7903  axpre-suploclemres  7996  elz  9356  elrp  9759  repos  10074  zsupssdc  10362  bitsfzolem  12184  isprm  12350  oddpwdc  12415  sqpweven  12416  2sqpwodd  12417  phimullem  12466  eulerthlem1  12468  eulerthlemfi  12469  eulerthlemrprm  12470  eulerthlemth  12473  hashgcdlem  12479  pclem0  12528  pclemub  12529  pclemdc  12530  pcprecl  12531  pcprendvds  12532  1arith  12609  elgz  12613  4sqlem13m  12645  4sqlem17  12649  4sqlem18  12650  ctiunctlemu1st  12724  ctiunctlemu2nd  12725  ctiunctlemudc  12727  ctiunctlemfo  12729  infpn2  12746  issgrp  13153  ismnddef  13168  gsumvallem2  13243  isgrp  13256  elnmz  13462  iscmn  13547  isrng  13614  issrg  13645  isring  13680  iscrng  13683  isnzr  13861  islring  13872  isrrg  13943  isdomn  13949  islmod  13971  psrbag  14349  psr1clfi  14368  isxms  14841  isms  14843  ivthinclemlm  15024  ivthinclemum  15025  ivthinclemlopn  15026  ivthinclemlr  15027  ivthinclemuopn  15028  ivthinclemur  15029  ivthinclemdisj  15030  ivthinclemloc  15031  mpodvdsmulf1o  15380  lgslem2  15396  lgslem3  15397  lgsfcl2  15401  0nninf  15805  nnsf  15806  peano4nninf  15807  nninfalllem1  15809  nninfself  15814  qdencn  15830