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  4579  regexmidlem1  4580  reg2exmidlema  4581  tfis  4630  ctssdccl  7212  nninff  7223  nninfninc  7224  infnninf  7225  infnninfOLD  7226  nnnninf  7227  nnnninfeq  7229  nnnninfeq2  7230  nninfwlpoimlemg  7276  exmidaclem  7319  ltexprlemell  7710  ltexprlemelu  7711  cauappcvgprlemm  7757  cauappcvgprlemopl  7758  cauappcvgprlemlol  7759  cauappcvgprlemopu  7760  cauappcvgprlemupu  7761  cauappcvgprlemdisj  7763  cauappcvgprlemloc  7764  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  cauappcvgprlem2  7772  caucvgprlemm  7780  caucvgprlemopl  7781  caucvgprlemlol  7782  caucvgprlemopu  7783  caucvgprlemupu  7784  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprlemladdfu  7789  caucvgprlem2  7792  caucvgprprlemell  7797  caucvgprprlemelu  7798  caucvgprprlemml  7806  caucvgprprlemmu  7807  caucvgprprlemexbt  7818  caucvgprprlem2  7822  suplocsrlemb  7918  suplocsrlempr  7919  suplocsrlem  7920  axpre-suploclemres  8013  elz  9373  elrp  9776  repos  10091  zsupssdc  10379  bitsfzolem  12207  isprm  12373  oddpwdc  12438  sqpweven  12439  2sqpwodd  12440  phimullem  12489  eulerthlem1  12491  eulerthlemfi  12492  eulerthlemrprm  12493  eulerthlemth  12496  hashgcdlem  12502  pclem0  12551  pclemub  12552  pclemdc  12553  pcprecl  12554  pcprendvds  12555  1arith  12632  elgz  12636  4sqlem13m  12668  4sqlem17  12672  4sqlem18  12673  ctiunctlemu1st  12747  ctiunctlemu2nd  12748  ctiunctlemudc  12750  ctiunctlemfo  12752  infpn2  12769  issgrp  13177  ismnddef  13192  gsumvallem2  13267  isgrp  13280  elnmz  13486  iscmn  13571  isrng  13638  issrg  13669  isring  13704  iscrng  13707  isnzr  13885  islring  13896  isrrg  13967  isdomn  13973  islmod  13995  psrbag  14373  psr1clfi  14392  isxms  14865  isms  14867  ivthinclemlm  15048  ivthinclemum  15049  ivthinclemlopn  15050  ivthinclemlr  15051  ivthinclemuopn  15052  ivthinclemur  15053  ivthinclemdisj  15054  ivthinclemloc  15055  mpodvdsmulf1o  15404  lgslem2  15420  lgslem3  15421  lgsfcl2  15425  0nninf  15874  nnsf  15875  peano4nninf  15876  nninfalllem1  15878  nninfself  15883  qdencn  15899