MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbcbidv Structured version   Visualization version   GIF version

Theorem sbcbidv 3688
Description: Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014.)
Hypothesis
Ref Expression
sbcbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
sbcbidv (𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem sbcbidv
StepHypRef Expression
1 nfv 2010 . 2 𝑥𝜑
2 sbcbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2sbcbid 3687 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  [wsbc 3633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-sbc 3634
This theorem is referenced by:  sbcbii  3689  opelopabsb  5181  opelopabgf  5191  opelopabf  5196  sbcfng  6253  sbcfg  6254  fmptsnd  6664  wrd2ind  13778  wrd2indOLD  13779  islmod  19185  elmptrab  21959  f1od2  30017  isomnd  30217  isorng  30315  indexa  34016  sdclem2  34025  sdclem1  34026  fdc  34028  sbcalf  34404  sbcexf  34405  hdmap1ffval  37816  hdmap1fval  37817  hdmapffval  37847  hdmapfval  37848  hgmapffval  37906  hgmapfval  37907  rexrabdioph  38144  rexfrabdioph  38145  2rexfrabdioph  38146  3rexfrabdioph  38147  4rexfrabdioph  38148  6rexfrabdioph  38149  7rexfrabdioph  38150  2sbc6g  39397  2sbc5g  39398
  Copyright terms: Public domain W3C validator