ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elrab2 GIF version

Theorem elrab2 2896
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
StepHypRef Expression
1 elrab2.2 . . 3 𝐶 = {𝑥𝐵𝜑}
21eleq2i 2244 . 2 (𝐴𝐶𝐴 ∈ {𝑥𝐵𝜑})
3 elrab2.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
43elrab 2893 . 2 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
52, 4bitri 184 1 (𝐴𝐶 ↔ (𝐴𝐵𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wcel 2148  {crab 2459
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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-v 2739
This theorem is referenced by:  elrabsf  3001  pwnss  4159  regexmidlemm  4531  regexmidlem1  4532  reg2exmidlema  4533  tfis  4582  ctssdccl  7109  nninff  7120  infnninf  7121  infnninfOLD  7122  nnnninf  7123  nnnninfeq  7125  nnnninfeq2  7126  nninfwlpoimlemg  7172  exmidaclem  7206  ltexprlemell  7596  ltexprlemelu  7597  cauappcvgprlemm  7643  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemopu  7646  cauappcvgprlemupu  7647  cauappcvgprlemdisj  7649  cauappcvgprlemloc  7650  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  cauappcvgprlem2  7658  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemopu  7669  caucvgprlemupu  7670  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemladdfu  7675  caucvgprlem2  7678  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemexbt  7704  caucvgprprlem2  7708  suplocsrlemb  7804  suplocsrlempr  7805  suplocsrlem  7806  axpre-suploclemres  7899  elz  9254  elrp  9654  repos  9969  zsupssdc  11954  isprm  12108  oddpwdc  12173  sqpweven  12174  2sqpwodd  12175  phimullem  12224  eulerthlem1  12226  eulerthlemfi  12227  eulerthlemrprm  12228  eulerthlemth  12231  hashgcdlem  12237  pclem0  12285  pclemub  12286  pclemdc  12287  pcprecl  12288  pcprendvds  12289  1arith  12364  elgz  12368  ctiunctlemu1st  12434  ctiunctlemu2nd  12435  ctiunctlemudc  12437  ctiunctlemfo  12439  infpn2  12456  issgrp  12808  ismnddef  12818  isgrp  12882  elnmz  13066  iscmn  13094  issrg  13146  isring  13181  iscrng  13184  isnzr  13323  islring  13331  islmod  13379  isxms  13921  isms  13923  ivthinclemlm  14082  ivthinclemum  14083  ivthinclemlopn  14084  ivthinclemlr  14085  ivthinclemuopn  14086  ivthinclemur  14087  ivthinclemdisj  14088  ivthinclemloc  14089  lgslem2  14372  lgslem3  14373  lgsfcl2  14377  0nninf  14723  nnsf  14724  peano4nninf  14725  nninfalllem1  14727  nninfself  14732  qdencn  14745
  Copyright terms: Public domain W3C validator