Theorem sbcbii 3776

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

Syntax hints:   ↔ wb 209  ⊤wtru 1539  [wsbc 3720

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sbc 3721

This theorem is referenced by:  eqsbc3r  3784  sbc3an  3785  sbccomlem  3799  sbccom  3800  sbcrext  3802  sbcabel  3807  csbcow  3843  csbco  3844  sbcnel12g  4319  sbcne12  4320  csbcom  4325  csbnestgfw  4327  csbnestgf  4332  sbccsb  4341  sbccsb2  4342  csbab  4345  2nreu  4349  sbcssg  4421  sbcop  5345  sbcrel  5619  difopab  5666  sbcfung  6348  tfinds2  7558  mpoxopovel  7869  f1od2  30483  bnj62  32100  bnj89  32101  bnj156  32108  bnj524  32118  bnj610  32128  bnj919  32148  bnj976  32159  bnj110  32240  bnj91  32243  bnj92  32244  bnj106  32250  bnj121  32252  bnj124  32253  bnj125  32254  bnj126  32255  bnj130  32256  bnj154  32260  bnj155  32261  bnj153  32262  bnj207  32263  bnj523  32269  bnj526  32270  bnj539  32273  bnj540  32274  bnj581  32290  bnj591  32293  bnj609  32299  bnj611  32300  bnj934  32317  bnj1000  32323  bnj984  32334  bnj985v  32335  bnj985  32336  bnj1040  32354  bnj1123  32368  bnj1452  32434  bnj1463  32437  sbcalf  35552  sbcexf  35553  sbccom2lem  35562  sbccom2  35563  sbccom2f  35564  sbccom2fi  35565  csbcom2fi  35566  2sbcrex  39725  2sbcrexOLD  39727  sbcrot3  39732  sbcrot5  39733  2rexfrabdioph  39737  3rexfrabdioph  39738  4rexfrabdioph  39739  6rexfrabdioph  39740  7rexfrabdioph  39741  rmydioph  39955  expdiophlem2  39963  sbcheg  40480  sbc3or  41238  trsbc  41246  onfrALTlem5  41248  eqsbc3rVD  41546  sbcoreleleqVD  41565  onfrALTlem5VD  41591  ich2exprop  43988