Theorem sbcan 3321

Description: Distribution of class substitution over conjunction. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 17-Aug-2018.)

Assertion

Ref	Expression
sbcan	|- ( [. A / x ]. ( ph /\ ps ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps ) )

Proof of Theorem sbcan

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sbcex 3288	. 2 |- ( [. A / x ]. ( ph /\ ps ) -> A e. _V )
2		sbcex 3288	. . 3 |- ( [. A / x ]. ps -> A e. _V )
3	2	adantl 472	. 2 |- ( ( [. A / x ]. ph /\ [. A / x ]. ps ) -> A e. _V )
4		dfsbcq2 3281	. . 3 |- ( y = A -> ( [ y / x ] ( ph /\ ps ) <-> [. A / x ]. ( ph /\ ps ) ) )
5		dfsbcq2 3281	. . . 4 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
6		dfsbcq2 3281	. . . 4 |- ( y = A -> ( [ y / x ] ps <-> [. A / x ]. ps ) )
7	5, 6	anbi12d 722	. . 3 |- ( y = A -> ( ( [ y / x ] ph /\ [ y / x ] ps ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps ) ) )
8		sban 2238	. . 3 |- ( [ y / x ] ( ph /\ ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) )
9	4, 7, 8	vtoclbg 3119	. 2 |- ( A e. _V -> ( [. A / x ]. ( ph /\ ps ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps ) ) )
10	1, 3, 9	pm5.21nii 359	1 |- ( [. A / x ]. ( ph /\ ps ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps ) )

Syntax hints:   <-> wb 189   /\ wa 375   = wceq 1454   [wsb 1807   e. wcel 1897   _Vcvv 3056   [.wsbc 3278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-v 3058  df-sbc 3279

This theorem is referenced by:  sbc3an  3336  sbcabel  3356  csbuni  4239  csbmpt12  4748  csbxp  4934  difopab  4984  sbcfung  5623  sbcfng  5747  sbcfg  5748  fmptsnd  6109  f1od2  28357  esum2dlem  28961  bnj976  29637  bnj110  29717  bnj1040  29829  csbopg2  31769  csbwrecsg  31772  csboprabg  31775  csbmpt22g  31776  f1omptsnlem  31782  mptsnunlem  31784  relowlpssretop  31811  csbfinxpg  31824  sbcani  32389  sbccom2lem  32408  brtrclfv2  36363  cotrclrcl  36378  frege124d  36397  sbiota1  36828  onfrALTlem5  36951  onfrALTlem4  36952