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

Theorem sbcbidv 3751
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 1890 . 2 𝑥𝜑
2 sbcbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2sbcbid 3750 1 (𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  [wsbc 3701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-12 2139  ax-ext 2767
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-sbc 3702
This theorem is referenced by:  sbcbii  3752  2nreu  4301  opelopabsb  5299  opelopabgf  5309  opelopabf  5314  sbcfng  6371  sbcfg  6372  fmptsnd  6785  wrd2ind  13909  islmod  19316  elmptrab  22107  f1od2  30118  isomnd  30332  isorng  30481  indexa  34486  sdclem2  34495  sdclem1  34496  fdc  34498  sbcalf  34872  sbcexf  34873  hdmap1ffval  38412  hdmap1fval  38413  hdmapffval  38443  hdmapfval  38444  hgmapffval  38502  hgmapfval  38503  rexrabdioph  38827  rexfrabdioph  38828  2rexfrabdioph  38829  3rexfrabdioph  38830  4rexfrabdioph  38831  6rexfrabdioph  38832  7rexfrabdioph  38833  2sbc6g  40237  2sbc5g  40238  or2expropbilem1  42737
  Copyright terms: Public domain W3C validator