Theorem sbcimg 3369

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1395   [wsb 1740   e. wcel 1819   [.wsbc 3327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-sbc 3328

This theorem is referenced by:  sbcim1  3376  sbceqal  3383  sbc19.21g  3398  sbcssg  3943  iota4an  5576  sbcfung  5617  riotass2  6284  tfinds2  6697  telgsums  17149  sbcimi  30717  sbcim2g  33452  sbcssOLD  33456  onfrALTlem5  33457  sbcim2gVD  33818  sbcssgVD  33826  onfrALTlem5VD  33828  bnj538OLD  33940  bnj110  34059  bnj92  34063  bnj539  34092  bnj540  34093  cdlemkid3N  36802  cdlemkid4  36803  cdlemk35s  36806  cdlemk39s  36808  cdlemk42  36810