Theorem sbcbii 2506

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

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298   e. wcel 1300  [wsbc 1534  _Vcvv 2292

This theorem is referenced by:  eqsbc3r 2507  sbc3angOLD 2509  sbcel1gvOLD 2511  sbcel2gvOLD 2513  sbcgfOLD 2521  sbc2iedv 2524  sbccomg 2526  sbcralt 2527  sbcrext 2528  sbcralgf 2529  sbcrexgf 2530  sbcabel 2535  csbcog 2547  sbcel12gOLD 2553  sbceqdigOLD 2555  sbccsbg 2565  sbccsb2g 2566  csbabg 2588  csbabgOLD 2589  foprab2 5061  fparlem1 5081  sbc3org 5827  trsbc 5843  bnj89 12444  bnj88 12447  bnj524 12523  bnj1046 12887  bnj1377 13095  bnj984 13358  bnj1462 13546  bnj1463 13550  sbcnel12g 16408  sbcne12g 16409  eqsbc3rVD 16664

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-sbc 2454

Copyright terms: Public domain