Theorem sbcbii 3798

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 3797	. 2 ⊢ (⊤ → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓))
4	3	mptru 1577	1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)

This proof depends on syntax axioms:   ↔ wb 209  ⊤wtru 1571  [wsbc 3742

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-sbc 3743

This theorem is used by:  eqsbc2  3805  sbc3an  3806  sbccom  3822  sbcrext  3824  sbcabel  3829  csbcow  3866  csbco  3867  sbcnel12g  4375  sbcne12  4376  csbcom  4381  csbnestgfw  4383  csbnestgf  4388  sbccsb  4397  sbccsb2  4398  csbab  4401  2nreu  4405  sbcssg  4480  sbcop  5464  sbcrel  5763  sbcfung  6586  sbcfungOLD  6587  tfinds2  7902  f1od2  8138  frpoins3xpg  8187  frpoins3xp3g  8188  mpoxopovel  8268  bnj62  35434  bnj89  35435  bnj156  35442  bnj524  35451  bnj610  35461  bnj919  35481  bnj976  35491  bnj110  35571  bnj91  35574  bnj92  35575  bnj106  35581  bnj121  35583  bnj124  35584  bnj125  35585  bnj126  35586  bnj130  35587  bnj154  35591  bnj155  35592  bnj153  35593  bnj207  35594  bnj523  35600  bnj526  35601  bnj539  35604  bnj540  35605  bnj581  35621  bnj591  35624  bnj609  35630  bnj611  35631  bnj934  35648  bnj1000  35654  bnj984  35665  bnj985v  35666  bnj985  35667  bnj1040  35685  bnj1123  35699  bnj1452  35765  bnj1463  35768  sbcalf  39249  sbcexf  39250  sbccom2lem  39259  sbccom2  39260  sbccom2f  39261  sbccom2fi  39262  csbcom2fi  39263  rspcsbnea  43384  2sbcrex  43999  sbcrot3  44002  sbcrot5  44003  2rexfrabdioph  44007  3rexfrabdioph  44008  4rexfrabdioph  44009  6rexfrabdioph  44010  7rexfrabdioph  44011  rmydioph  44225  expdiophlem2  44233  sbcheg  44982  sbc3or  45717  trsbc  45725  onfrALTlem5  45727  eqsbc2VD  46024  sbcoreleleqVD  46043  onfrALTlem5VD  46069  ich2exprop  48768