Theorem sbcimg 3320

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 3281	. 2 |- ( y = A -> ( [ y / x ] ( ph -> ps ) <-> [. A / x ]. ( ph -> ps ) ) )
2		dfsbcq2 3281	. . 3 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
3		dfsbcq2 3281	. . 3 |- ( y = A -> ( [ y / x ] ps <-> [. A / x ]. ps ) )
4	2, 3	imbi12d 326	. 2 |- ( y = A -> ( ( [ y / x ] ph -> [ y / x ] ps ) <-> ( [. A / x ]. ph -> [. A / x ]. ps ) ) )
5		sbim 2234	. 2 |- ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> [ y / x ] ps ) )
6	1, 4, 5	vtoclbg 3119	1 |- ( A e. V -> ( [. A / x ]. ( ph -> ps ) <-> ( [. A / x ]. ph -> [. A / x ]. ps ) ) )

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1454   [wsb 1807   e. wcel 1897   [.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:  sbcim1  3325  sbceqal  3330  sbc19.21g  3343  sbcssg  3891  iota4an  5583  sbcfung  5623  riotass2  6302  tfinds2  6716  telgsums  17671  bnj538OLD  29598  bnj110  29717  bnj92  29721  bnj539  29750  bnj540  29751  f1omptsnlem  31782  mptsnunlem  31784  topdifinffinlem  31794  relowlpssretop  31811  rdgeqoa  31817  sbcimi  32391  cdlemkid3N  34544  cdlemkid4  34545  cdlemk35s  34548  cdlemk39s  34550  cdlemk42  34552  frege77  36580  frege116  36619  frege118  36621  sbcim2g  36942  sbcssOLD  36950  onfrALTlem5  36951  sbcim2gVD  37311  sbcssgVD  37319  onfrALTlem5VD  37321  iccelpart  38784