Theorem sbcbidv 3490

Description: Formula-building deduction rule for class substitution. (Contributed by NM, 29-Dec-2014.)

Hypothesis

Ref	Expression
sbcbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

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

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem sbcbidv

Step	Hyp	Ref	Expression
1		nfv 1843	. 2 |- F/ x ph
2		sbcbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	sbcbid 3489	1 |- ( ph -> ( [. A / x ]. ps <-> [. A / x ]. ch ) )

Syntax hints:   -> wi 4   <-> wb 196   [.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-11 2034  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-sbc 3436

This theorem is referenced by:  sbcbii  3491  opelopabsb  4985  opelopabgf  4995  opelopabf  5000  sbcfng  6042  sbcfg  6043  fmptsnd  6435  wrd2ind  13477  islmod  18867  elmptrab  21630  f1od2  29499  isomnd  29701  isorng  29799  indexa  33528  sdclem2  33538  sdclem1  33539  fdc  33541  sbcalf  33917  sbcexf  33918  hdmap1ffval  37085  hdmap1fval  37086  hdmapffval  37118  hdmapfval  37119  hgmapffval  37177  hgmapfval  37178  rexrabdioph  37358  rexfrabdioph  37359  2rexfrabdioph  37360  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  2sbc6g  38616  2sbc5g  38617