Theorem sbcbii 3785

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

Syntax hints:   ↔ wb 206  ⊤wtru 1543  [wsbc 3728

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3729

This theorem is referenced by:  eqsbc2  3792  sbc3an  3793  sbccomlemOLD  3808  sbccom  3809  sbcrext  3811  sbcabel  3816  csbcow  3852  csbco  3853  sbcnel12g  4354  sbcne12  4355  csbcom  4360  csbnestgfw  4362  csbnestgf  4367  sbccsb  4376  sbccsb2  4377  csbab  4380  2nreu  4384  sbcssg  4461  sbcop  5442  sbcrel  5737  sbcfung  6522  tfinds2  7815  frpoins3xpg  8090  frpoins3xp3g  8091  mpoxopovel  8170  f1od2  32792  bnj62  34863  bnj89  34864  bnj156  34871  bnj524  34880  bnj610  34890  bnj919  34910  bnj976  34920  bnj110  35000  bnj91  35003  bnj92  35004  bnj106  35010  bnj121  35012  bnj124  35013  bnj125  35014  bnj126  35015  bnj130  35016  bnj154  35020  bnj155  35021  bnj153  35022  bnj207  35023  bnj523  35029  bnj526  35030  bnj539  35033  bnj540  35034  bnj581  35050  bnj591  35053  bnj609  35059  bnj611  35060  bnj934  35077  bnj1000  35083  bnj984  35094  bnj985v  35095  bnj985  35096  bnj1040  35114  bnj1123  35128  bnj1452  35194  bnj1463  35197  sbcalf  38435  sbcexf  38436  sbccom2lem  38445  sbccom2  38446  sbccom2f  38447  sbccom2fi  38448  csbcom2fi  38449  rspcsbnea  42570  2sbcrex  43216  sbcrot3  43219  sbcrot5  43220  2rexfrabdioph  43224  3rexfrabdioph  43225  4rexfrabdioph  43226  6rexfrabdioph  43227  7rexfrabdioph  43228  rmydioph  43442  expdiophlem2  43450  sbcheg  44206  sbc3or  44959  trsbc  44967  onfrALTlem5  44969  eqsbc2VD  45266  sbcoreleleqVD  45285  onfrALTlem5VD  45311  ich2exprop  47931