Theorem sbcbii 1974

Description: Formula-building inference rule for class substitution.

Hypothesis

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

Assertion

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

Proof of Theorem sbcbii

Step	Hyp	Ref	Expression
1		eqid 1473	. 2 |- V = V
2		sbcbii.1	. . . 4 |- (ph <-> ps)
3	2	a1i 8	. . 3 |- (V = V -> (ph <-> ps))
4	3	sbcbidv 1973	. 2 |- ((V = V /\ A e. B) -> ([A / x]ph <-> [A / x]ps))
5	1, 4	mpan 694	1 |- (A e. B -> ([A / x]ph <-> [A / x]ps))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 954   e. wcel 956  [wsbc 1168  Vcvv 1807

This theorem is referenced by:  sbc3ang 1975  sbcel1gv 1976  sbcel2gv 1977  sbcgf 1982  sbccomg 1985  sbcralt 1986  sbcrext 1987  sbcralgf 1988  sbcrexgf 1989  sbcabel 1992  csbcog 2003  sbcel12g 2007  sbceqdig 2008  sbccsbg 2018  sbccsb2g 2019  csbabg 2039  dfoprab5 4105  foprab2 4109

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-sbc 1938

Copyright terms: Public domain