Theorem sbcan 3828

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 3786	. 2 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) → 𝐴 ∈ V)
2		sbcex 3786	. . 3 ⊢ ([𝐴 / 𝑥]𝜓 → 𝐴 ∈ V)
3	2	adantl 482	. 2 ⊢ (([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓) → 𝐴 ∈ V)
4		dfsbcq2 3779	. . 3 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ [𝐴 / 𝑥](𝜑 ∧ 𝜓)))
5		dfsbcq2 3779	. . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
6		dfsbcq2 3779	. . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜓))
7	5, 6	anbi12d 631	. . 3 ⊢ (𝑦 = 𝐴 → (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓)))
8		sban 2083	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
9	4, 7, 8	vtoclbg 3559	. 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓)))
10	1, 3, 9	pm5.21nii 379	1 ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∧ [𝐴 / 𝑥]𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1541  [wsb 2067   ∈ wcel 2106  Vcvv 3474  [wsbc 3776

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-sbc 3777

This theorem is referenced by:  sbc3an  3846  sbcabel  3871  2nreu  4440  csbopg  4890  csbuni  4939  csbmpt12  5556  csbxp  5773  difopabOLD  5829  sbcfung  6569  sbcfng  6711  sbcfg  6712  fmptsnd  7163  csbfrecsg  8265  f1od2  31933  esum2dlem  33078  bnj976  33776  bnj110  33857  bnj1040  33971  csboprabg  36199  csbmpo123  36200  f1omptsnlem  36205  mptsnunlem  36207  relowlpssretop  36233  csbfinxpg  36257  sbcani  36964  sbccom2lem  36980  minregex  42270  brtrclfv2  42463  cotrclrcl  42478  frege124d  42497  sbiota1  43178  onfrALTlem5  43288  onfrALTlem4  43289  csbingVD  43630  onfrALTlem5VD  43631  onfrALTlem4VD  43632  csbxpgVD  43640  csbunigVD  43644