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

Theorem sbcbidv 3457
 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 1830 . 2 𝑥𝜑
2 sbcbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2sbcbid 3456 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  [wsbc 3402 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-sbc 3403 This theorem is referenced by:  sbcbii  3458  opelopabsb  4910  opelopabgf  4920  opelopabf  4925  sbcfng  5955  sbcfg  5956  fmptsnd  6340  wrd2ind  13329  islmod  18690  elmptrab  21440  nbgraopALT  25953  f1od2  28887  isomnd  29032  isorng  29130  indexa  32698  sdclem2  32708  sdclem1  32709  fdc  32711  sbcalf  33087  sbcexf  33088  hdmap1ffval  36103  hdmap1fval  36104  hdmapffval  36136  hdmapfval  36137  hgmapffval  36195  hgmapfval  36196  rexrabdioph  36376  rexfrabdioph  36377  2rexfrabdioph  36378  3rexfrabdioph  36379  4rexfrabdioph  36380  6rexfrabdioph  36381  7rexfrabdioph  36382  2sbc6g  37638  2sbc5g  37639
 Copyright terms: Public domain W3C validator