Theorem sbcbii 3794

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

Syntax hints:   ↔ wb 206  ⊤wtru 1542  [wsbc 3737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-sbc 3738

This theorem is referenced by:  eqsbc2  3801  sbc3an  3802  sbccomlemOLD  3817  sbccom  3818  sbcrext  3820  sbcabel  3825  csbcow  3861  csbco  3862  sbcnel12g  4363  sbcne12  4364  csbcom  4369  csbnestgfw  4371  csbnestgf  4376  sbccsb  4385  sbccsb2  4386  csbab  4389  2nreu  4393  sbcssg  4471  sbcop  5434  sbcrel  5727  sbcfung  6512  tfinds2  7802  frpoins3xpg  8078  frpoins3xp3g  8079  mpoxopovel  8158  f1od2  32708  bnj62  34755  bnj89  34756  bnj156  34763  bnj524  34772  bnj610  34782  bnj919  34802  bnj976  34812  bnj110  34893  bnj91  34896  bnj92  34897  bnj106  34903  bnj121  34905  bnj124  34906  bnj125  34907  bnj126  34908  bnj130  34909  bnj154  34913  bnj155  34914  bnj153  34915  bnj207  34916  bnj523  34922  bnj526  34923  bnj539  34926  bnj540  34927  bnj581  34943  bnj591  34946  bnj609  34952  bnj611  34953  bnj934  34970  bnj1000  34976  bnj984  34987  bnj985v  34988  bnj985  34989  bnj1040  35007  bnj1123  35021  bnj1452  35087  bnj1463  35090  sbcalf  38177  sbcexf  38178  sbccom2lem  38187  sbccom2  38188  sbccom2f  38189  sbccom2fi  38190  csbcom2fi  38191  rspcsbnea  42247  2sbcrex  42904  2sbcrexOLD  42906  sbcrot3  42911  sbcrot5  42912  2rexfrabdioph  42916  3rexfrabdioph  42917  4rexfrabdioph  42918  6rexfrabdioph  42919  7rexfrabdioph  42920  rmydioph  43134  expdiophlem2  43142  sbcheg  43899  sbc3or  44652  trsbc  44660  onfrALTlem5  44662  eqsbc2VD  44959  sbcoreleleqVD  44978  onfrALTlem5VD  45004  ich2exprop  47598