Theorem sbcimg 3477

Description: Distribution of class substitution over implication. (Contributed by NM, 16-Jan-2004.)

Assertion

Ref	Expression
sbcimg	|- ( A e. V -> ( [. A / x ]. ( ph -> ps ) <-> ( [. A / x ]. ph -> [. A / x ]. ps ) ) )

Proof of Theorem sbcimg

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsbcq2 3438	. 2 |- ( y = A -> ( [ y / x ] ( ph -> ps ) <-> [. A / x ]. ( ph -> ps ) ) )
2		dfsbcq2 3438	. . 3 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
3		dfsbcq2 3438	. . 3 |- ( y = A -> ( [ y / x ] ps <-> [. A / x ]. ps ) )
4	2, 3	imbi12d 334	. 2 |- ( y = A -> ( ( [ y / x ] ph -> [ y / x ] ps ) <-> ( [. A / x ]. ph -> [. A / x ]. ps ) ) )
5		sbim 2395	. 2 |- ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> [ y / x ] ps ) )
6	1, 4, 5	vtoclbg 3267	1 |- ( A e. V -> ( [. A / x ]. ( ph -> ps ) <-> ( [. A / x ]. ph -> [. A / x ]. ps ) ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   [wsb 1880   e. wcel 1990   [.wsbc 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202  df-sbc 3436

This theorem is referenced by:  sbcim1  3482  sbceqal  3487  sbc19.21g  3502  sbcssg  4085  iota4an  5870  sbcfung  5912  riotass2  6638  tfinds2  7063  telgsums  18390  bnj538OLD  30810  bnj110  30928  bnj92  30932  bnj539  30961  bnj540  30962  f1omptsnlem  33183  mptsnunlem  33185  topdifinffinlem  33195  relowlpssretop  33212  rdgeqoa  33218  sbcimi  33912  cdlemkid3N  36221  cdlemkid4  36222  cdlemk35s  36225  cdlemk39s  36227  cdlemk42  36229  frege77  38234  frege116  38273  frege118  38275  sbcim2g  38748  sbcssOLD  38756  onfrALTlem5  38757  sbcim2gVD  39111  sbcssgVD  39119  onfrALTlem5VD  39121  iccelpart  41369