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

Theorem sbcbidv 3631
Description: Formula-building deduction rule 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 1992 . 2 𝑥𝜑
2 sbcbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2sbcbid 3630 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  [wsbc 3576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-sbc 3577
This theorem is referenced by:  sbcbii  3632  opelopabsb  5135  opelopabgf  5145  opelopabf  5150  sbcfng  6203  sbcfg  6204  fmptsnd  6600  wrd2ind  13697  islmod  19089  elmptrab  21852  f1od2  29829  isomnd  30031  isorng  30129  indexa  33859  sdclem2  33869  sdclem1  33870  fdc  33872  sbcalf  34248  sbcexf  34249  hdmap1ffval  37605  hdmap1fval  37606  hdmapffval  37638  hdmapfval  37639  hgmapffval  37697  hgmapfval  37698  rexrabdioph  37878  rexfrabdioph  37879  2rexfrabdioph  37880  3rexfrabdioph  37881  4rexfrabdioph  37882  6rexfrabdioph  37883  7rexfrabdioph  37884  2sbc6g  39136  2sbc5g  39137
  Copyright terms: Public domain W3C validator