Theorem sbcbii 1978

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 1475	. 2 |- V = V
2		sbcbii.1	. . . 4 |- (ph <-> ps)
3	2	a1i 8	. . 3 |- (V = V -> (ph <-> ps))
4	3	sbcbidv 1977	. 2 |- ((V = V /\ A e. B) -> ([A / x]ph <-> [A / x]ps))
5	1, 4	mpan 695	1 |- (A e. B -> ([A / x]ph <-> [A / x]ps))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956   e. wcel 958  [wsbc 1170  Vcvv 1811

This theorem is referenced by:  sbc3ang 1979  sbcel1gv 1980  sbcel2gv 1981  sbcgf 1986  sbccomg 1989  sbcralt 1990  sbcrext 1991  sbcralgf 1992  sbcrexgf 1993  sbcabel 1996  csbcog 2007  sbcel12g 2011  sbceqdig 2012  sbccsbg 2022  sbccsb2g 2023  csbabg 2043  dfoprab5 4115  foprab2 4119

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-sbc 1942

Copyright terms: Public domain