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

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

Proof of Theorem sbcbidv
StepHypRef Expression
1 eqidd 2799 . 2 (𝜑𝐴 = 𝐴)
2 sbcbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2sbceqbid 3729 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  [wsbc 3722 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sbc 3723 This theorem is referenced by:  sbcbii  3778  2nreu  4352  opelopabsb  5386  opelopabgf  5396  opelopabf  5401  sbcfng  6492  sbcfg  6493  fmptsnd  6918  wrd2ind  14096  islmod  19652  elmptrab  22473  f1od2  30527  isomnd  30801  isorng  30972  indexa  35322  sdclem2  35331  sdclem1  35332  fdc  35334  sbcalf  35703  sbcexf  35704  hdmap1ffval  39242  hdmap1fval  39243  hdmapffval  39273  hdmapfval  39274  hgmapffval  39332  hgmapfval  39333  rexrabdioph  39906  rexfrabdioph  39907  2rexfrabdioph  39908  3rexfrabdioph  39909  4rexfrabdioph  39910  6rexfrabdioph  39911  7rexfrabdioph  39912  2sbc6g  41290  2sbc5g  41291  or2expropbilem1  43792
 Copyright terms: Public domain W3C validator