Theorem elrab2 2962

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 2959	. 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 2801

This theorem is referenced by:  elrabsf  3067  pwnss  4243  regexmidlemm  4624  regexmidlem1  4625  reg2exmidlema  4626  tfis  4675  ctssdccl  7289  nninff  7300  nninfninc  7301  infnninf  7302  infnninfOLD  7303  nnnninf  7304  nnnninfeq  7306  nnnninfeq2  7307  nninfwlpoimlemg  7353  exmidaclem  7401  ltexprlemell  7796  ltexprlemelu  7797  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemopu  7846  cauappcvgprlemupu  7847  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem2  7858  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemopu  7869  caucvgprlemupu  7870  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemladdfu  7875  caucvgprlem2  7878  caucvgprprlemell  7883  caucvgprprlemelu  7884  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemexbt  7904  caucvgprprlem2  7908  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  axpre-suploclemres  8099  elz  9459  elrp  9863  repos  10178  zsupssdc  10470  bitsfzolem  12480  isprm  12646  oddpwdc  12711  sqpweven  12712  2sqpwodd  12713  phimullem  12762  eulerthlem1  12764  eulerthlemfi  12765  eulerthlemrprm  12766  eulerthlemth  12769  hashgcdlem  12775  pclem0  12824  pclemub  12825  pclemdc  12826  pcprecl  12827  pcprendvds  12828  1arith  12905  elgz  12909  4sqlem13m  12941  4sqlem17  12945  4sqlem18  12946  ctiunctlemu1st  13020  ctiunctlemu2nd  13021  ctiunctlemudc  13023  ctiunctlemfo  13025  infpn2  13042  issgrp  13451  ismnddef  13466  gsumvallem2  13541  isgrp  13554  elnmz  13760  iscmn  13845  isrng  13912  issrg  13943  isring  13978  iscrng  13981  isnzr  14160  islring  14171  isrrg  14242  isdomn  14248  islmod  14270  psrbag  14648  psr1clfi  14667  isxms  15140  isms  15142  ivthinclemlm  15323  ivthinclemum  15324  ivthinclemlopn  15325  ivthinclemlr  15326  ivthinclemuopn  15327  ivthinclemur  15328  ivthinclemdisj  15329  ivthinclemloc  15330  mpodvdsmulf1o  15679  lgslem2  15695  lgslem3  15696  lgsfcl2  15700  lfgredg2dom  15945  uspgredg2vlem  16033  uspgredg2v  16034  usgredg2vlem1  16035  usgredg2vlem2  16036  ushgredgedg  16039  ushgredgedgloop  16041  0nninf  16430  nnsf  16431  peano4nninf  16432  nninfalllem1  16434  nninfself  16439  qdencn  16455