Theorem sbcan 3367

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 3334	. 2 |- ( [. A / x ]. ( ph /\ ps ) -> A e. _V )
2		sbcex 3334	. . 3 |- ( [. A / x ]. ps -> A e. _V )
3	2	adantl 464	. 2 |- ( ( [. A / x ]. ph /\ [. A / x ]. ps ) -> A e. _V )
4		dfsbcq2 3327	. . 3 |- ( y = A -> ( [ y / x ] ( ph /\ ps ) <-> [. A / x ]. ( ph /\ ps ) ) )
5		dfsbcq2 3327	. . . 4 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
6		dfsbcq2 3327	. . . 4 |- ( y = A -> ( [ y / x ] ps <-> [. A / x ]. ps ) )
7	5, 6	anbi12d 708	. . 3 |- ( y = A -> ( ( [ y / x ] ph /\ [ y / x ] ps ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps ) ) )
8		sban 2142	. . 3 |- ( [ y / x ] ( ph /\ ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) )
9	4, 7, 8	vtoclbg 3165	. 2 |- ( A e. _V -> ( [. A / x ]. ( ph /\ ps ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps ) ) )
10	1, 3, 9	pm5.21nii 351	1 |- ( [. A / x ]. ( ph /\ ps ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps ) )

Syntax hints:   <-> wb 184   /\ wa 367   = wceq 1398   [wsb 1744   e. wcel 1823   _Vcvv 3106   [.wsbc 3324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3108  df-sbc 3325

This theorem is referenced by:  sbc3an  3382  sbcabel  3402  csbuni  4263  csbmpt12  4770  csbxp  5070  difopab  5123  sbcfung  5593  sbcfng  5710  sbcfg  5711  fmptsnd  6069  f1od2  27781  esum2dlem  28324  sbcani  30753  sbccom2lem  30772  sbiota1  31585  onfrALTlem5  33727  onfrALTlem4  33728  bnj976  34256  bnj110  34336  bnj1040  34448  cotrclrcl  38253  brtrclfv2  38261