Theorem sbcbii 3837

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

Syntax hints:   ↔ wb 205  ⊤wtru 1542  [wsbc 3777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-sbc 3778

This theorem is referenced by:  eqsbc2  3846  sbc3an  3847  sbccomlem  3864  sbccom  3865  sbcrext  3867  sbcabel  3872  csbcow  3908  csbco  3909  sbcnel12g  4411  sbcne12  4412  csbcom  4417  csbnestgfw  4419  csbnestgf  4424  sbccsb  4433  sbccsb2  4434  csbab  4437  2nreu  4441  sbcssg  4523  sbcop  5489  sbcrel  5780  difopabOLD  5831  sbcfung  6572  tfinds2  7855  frpoins3xpg  8128  frpoins3xp3g  8129  mpoxopovel  8207  f1od2  32201  bnj62  34017  bnj89  34018  bnj156  34025  bnj524  34034  bnj610  34044  bnj919  34064  bnj976  34074  bnj110  34155  bnj91  34158  bnj92  34159  bnj106  34165  bnj121  34167  bnj124  34168  bnj125  34169  bnj126  34170  bnj130  34171  bnj154  34175  bnj155  34176  bnj153  34177  bnj207  34178  bnj523  34184  bnj526  34185  bnj539  34188  bnj540  34189  bnj581  34205  bnj591  34208  bnj609  34214  bnj611  34215  bnj934  34232  bnj1000  34238  bnj984  34249  bnj985v  34250  bnj985  34251  bnj1040  34269  bnj1123  34283  bnj1452  34349  bnj1463  34352  sbcalf  37285  sbcexf  37286  sbccom2lem  37295  sbccom2  37296  sbccom2f  37297  sbccom2fi  37298  csbcom2fi  37299  2sbcrex  41824  2sbcrexOLD  41826  sbcrot3  41831  sbcrot5  41832  2rexfrabdioph  41836  3rexfrabdioph  41837  4rexfrabdioph  41838  6rexfrabdioph  41839  7rexfrabdioph  41840  rmydioph  42055  expdiophlem2  42063  sbcheg  42832  sbc3or  43595  trsbc  43603  onfrALTlem5  43605  eqsbc2VD  43903  sbcoreleleqVD  43922  onfrALTlem5VD  43948  ich2exprop  46438