Theorem sbcbii 3772

Description: Formula-building inference for class substitution. (Contributed by NM, 11-Nov-2005.)

Hypothesis

Ref	Expression
sbcbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
sbcbii	⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)

Proof of Theorem sbcbii

Step	Hyp	Ref	Expression
1		sbcbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓))
3	2	sbcbidv 3770	. 2 ⊢ (⊤ → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))
4	3	mptru 1546	1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)

Syntax hints:   ↔ wb 205  ⊤wtru 1540  [wsbc 3711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sbc 3712

This theorem is referenced by:  eqsbc2  3781  sbc3an  3782  sbccomlem  3799  sbccom  3800  sbcrext  3802  sbcabel  3807  csbcow  3843  csbco  3844  sbcnel12g  4342  sbcne12  4343  csbcom  4348  csbnestgfw  4350  csbnestgf  4355  sbccsb  4364  sbccsb2  4365  csbab  4368  2nreu  4372  sbcssg  4451  sbcop  5397  sbcrel  5681  difopab  5729  sbcfung  6442  tfinds2  7685  mpoxopovel  8007  f1od2  30958  bnj62  32599  bnj89  32600  bnj156  32607  bnj524  32617  bnj610  32627  bnj919  32647  bnj976  32657  bnj110  32738  bnj91  32741  bnj92  32742  bnj106  32748  bnj121  32750  bnj124  32751  bnj125  32752  bnj126  32753  bnj130  32754  bnj154  32758  bnj155  32759  bnj153  32760  bnj207  32761  bnj523  32767  bnj526  32768  bnj539  32771  bnj540  32772  bnj581  32788  bnj591  32791  bnj609  32797  bnj611  32798  bnj934  32815  bnj1000  32821  bnj984  32832  bnj985v  32833  bnj985  32834  bnj1040  32852  bnj1123  32866  bnj1452  32932  bnj1463  32935  frpoins3xpg  33714  frpoins3xp3g  33715  sbcalf  36199  sbcexf  36200  sbccom2lem  36209  sbccom2  36210  sbccom2f  36211  sbccom2fi  36212  csbcom2fi  36213  2sbcrex  40522  2sbcrexOLD  40524  sbcrot3  40529  sbcrot5  40530  2rexfrabdioph  40534  3rexfrabdioph  40535  4rexfrabdioph  40536  6rexfrabdioph  40537  7rexfrabdioph  40538  rmydioph  40752  expdiophlem2  40760  sbcheg  41276  sbc3or  42041  trsbc  42049  onfrALTlem5  42051  eqsbc2VD  42349  sbcoreleleqVD  42368  onfrALTlem5VD  42394  ich2exprop  44811