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

Theorem sbcan 3829
Description: Distribution of class substitution over conjunction. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 17-Aug-2018.)
Assertion
Ref Expression
sbcan ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))

Proof of Theorem sbcan
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 sbcex 3786 . 2 ([𝐴 / 𝑥](𝜑𝜓) → 𝐴 ∈ V)
2 sbcex 3786 . . 3 ([𝐴 / 𝑥]𝜓𝐴 ∈ V)
32adantl 481 . 2 (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) → 𝐴 ∈ V)
4 dfsbcq2 3779 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑𝜓) ↔ [𝐴 / 𝑥](𝜑𝜓)))
5 dfsbcq2 3779 . . . 4 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
6 dfsbcq2 3779 . . . 4 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓[𝐴 / 𝑥]𝜓))
75, 6anbi12d 631 . . 3 (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
8 sban 2076 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
94, 7, 8vtoclbg 3542 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
101, 3, 9pm5.21nii 378 1 ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 395   = wceq 1534  [wsb 2060  wcel 2099  Vcvv 3471  [wsbc 3776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-sbc 3777
This theorem is referenced by:  sbc3an  3846  sbcabel  3871  2nreu  4442  csbopg  4892  csbuni  4939  csbmpt12  5559  csbxp  5777  difopabOLD  5833  sbcfung  6577  sbcfng  6719  sbcfg  6720  fmptsnd  7178  csbfrecsg  8290  f1od2  32516  esum2dlem  33711  bnj976  34408  bnj110  34489  bnj1040  34603  csboprabg  36809  csbmpo123  36810  f1omptsnlem  36815  mptsnunlem  36817  relowlpssretop  36843  csbfinxpg  36867  sbcani  37581  sbccom2lem  37597  minregex  42964  brtrclfv2  43157  cotrclrcl  43172  frege124d  43191  sbiota1  43871  onfrALTlem5  43981  onfrALTlem4  43982  csbingVD  44323  onfrALTlem5VD  44324  onfrALTlem4VD  44325  csbxpgVD  44333  csbunigVD  44337
  Copyright terms: Public domain W3C validator