Theorem sbcan 3791

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.

Step	Hyp	Ref	Expression
1		sbcex 3751	. 2 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) → 𝐴 ∈ V)
2		sbcex 3751	. . 3 ⊢ ([𝐴 / 𝑥]𝜓 → 𝐴 ∈ V)
3	2	adantl 481	. 2 ⊢ (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓) → 𝐴 ∈ V)
4		dfsbcq2 3744	. . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ [𝐴 / 𝑥](𝜑 ∧ 𝜓)))
5		dfsbcq2 3744	. . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
6		dfsbcq2 3744	. . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜓))
7	5, 6	anbi12d 632	. . 3 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓)))
8		sban 2083	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
9	4, 7, 8	vtoclbg 3512	. 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓)))
10	1, 3, 9	pm5.21nii 378	1 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541  [wsb 2067   ∈ wcel 2111  Vcvv 3436  [wsbc 3741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-sbc 3742

This theorem is referenced by:  sbc3an  3806  sbcabel  3829  2nreu  4394  csbopg  4843  csbuni  4888  csbmpt12  5497  csbxp  5716  sbcfung  6505  sbcfng  6648  sbcfg  6649  fmptsnd  7103  csbfrecsg  8214  f1od2  32700  esum2dlem  34103  bnj976  34787  bnj110  34868  bnj1040  34982  csboprabg  37370  csbmpo123  37371  f1omptsnlem  37376  mptsnunlem  37378  relowlpssretop  37404  csbfinxpg  37428  sbcani  38154  sbccom2lem  38170  minregex  43573  brtrclfv2  43766  cotrclrcl  43781  frege124d  43800  sbiota1  44473  onfrALTlem5  44581  onfrALTlem4  44582  csbingVD  44922  onfrALTlem5VD  44923  onfrALTlem4VD  44924  csbxpgVD  44932  csbunigVD  44936  rspesbcd  44976