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

Theorem elrab2 2772
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 2154 . 2 (𝐴𝐶𝐴 ∈ {𝑥𝐵𝜑})
3 elrab2.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
43elrab 2769 . 2 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
52, 4bitri 182 1 (𝐴𝐶 ↔ (𝐴𝐵𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103   = wceq 1289  wcel 1438  {crab 2363
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rab 2368  df-v 2621
This theorem is referenced by:  elrabsf  2875  pwnss  3986  regexmidlemm  4338  regexmidlem1  4339  reg2exmidlema  4340  tfis  4388  infnninf  6784  nnnninf  6785  ltexprlemell  7136  ltexprlemelu  7137  cauappcvgprlemm  7183  cauappcvgprlemopl  7184  cauappcvgprlemlol  7185  cauappcvgprlemopu  7186  cauappcvgprlemupu  7187  cauappcvgprlemdisj  7189  cauappcvgprlemloc  7190  cauappcvgprlemladdfu  7192  cauappcvgprlemladdfl  7193  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  cauappcvgprlem2  7198  caucvgprlemm  7206  caucvgprlemopl  7207  caucvgprlemlol  7208  caucvgprlemopu  7209  caucvgprlemupu  7210  caucvgprlemdisj  7212  caucvgprlemloc  7213  caucvgprlemladdfu  7215  caucvgprlem2  7218  caucvgprprlemell  7223  caucvgprprlemelu  7224  caucvgprprlemml  7232  caucvgprprlemmu  7233  caucvgprprlemexbt  7244  caucvgprprlem2  7248  elz  8722  elrp  9105  repos  9357  isprm  11173  oddpwdc  11234  sqpweven  11235  2sqpwodd  11236  phimullem  11283  hashgcdlem  11285  0nninf  11539  nninff  11540  nnsf  11541  peano4nninf  11542  nninfalllemn  11544  nninfalllem1  11545  nninfself  11551  qdencn  11561
  Copyright terms: Public domain W3C validator