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

Theorem elab2 2803
 Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
Hypotheses
Ref Expression
elab2.1 𝐴 ∈ V
elab2.2 (𝑥 = 𝐴 → (𝜑𝜓))
elab2.3 𝐵 = {𝑥𝜑}
Assertion
Ref Expression
elab2 (𝐴𝐵𝜓)
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem elab2
StepHypRef Expression
1 elab2.1 . 2 𝐴 ∈ V
2 elab2.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
3 elab2.3 . . 3 𝐵 = {𝑥𝜑}
42, 3elab2g 2802 . 2 (𝐴 ∈ V → (𝐴𝐵𝜓))
51, 4ax-mp 5 1 (𝐴𝐵𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   = wceq 1314   ∈ wcel 1463  {cab 2101  Vcvv 2658 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-v 2660 This theorem is referenced by:  elpw  3484  elint  3745  opabid  4147  elrn2  4749  elimasn  4874  oprabid  5769  tfrlem3a  6173  tfrcllemsucaccv  6217  tfrcllembxssdm  6219  tfrcllemres  6225  addnqprlemrl  7329  addnqprlemru  7330  addnqprlemfl  7331  addnqprlemfu  7332  mulnqprlemrl  7345  mulnqprlemru  7346  mulnqprlemfl  7347  mulnqprlemfu  7348  ltnqpr  7365  ltnqpri  7366  archpr  7415  cauappcvgprlemladdfu  7426  cauappcvgprlemladdfl  7427  caucvgprlemladdfu  7449  caucvgprprlemopu  7471  suplocexprlemloc  7493  txuni2  12331
 Copyright terms: Public domain W3C validator