Theorem sbcbii 3786

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3730

This theorem is referenced by:  eqsbc2  3793  sbc3an  3794  sbccomlemOLD  3809  sbccom  3810  sbcrext  3812  sbcabel  3817  csbcow  3853  csbco  3854  sbcnel12g  4355  sbcne12  4356  csbcom  4361  csbnestgfw  4363  csbnestgf  4368  sbccsb  4377  sbccsb2  4378  csbab  4381  2nreu  4385  sbcssg  4462  sbcop  5437  sbcrel  5730  sbcfung  6516  tfinds2  7808  frpoins3xpg  8083  frpoins3xp3g  8084  mpoxopovel  8163  f1od2  32807  bnj62  34879  bnj89  34880  bnj156  34887  bnj524  34896  bnj610  34906  bnj919  34926  bnj976  34936  bnj110  35016  bnj91  35019  bnj92  35020  bnj106  35026  bnj121  35028  bnj124  35029  bnj125  35030  bnj126  35031  bnj130  35032  bnj154  35036  bnj155  35037  bnj153  35038  bnj207  35039  bnj523  35045  bnj526  35046  bnj539  35049  bnj540  35050  bnj581  35066  bnj591  35069  bnj609  35075  bnj611  35076  bnj934  35093  bnj1000  35099  bnj984  35110  bnj985v  35111  bnj985  35112  bnj1040  35130  bnj1123  35144  bnj1452  35210  bnj1463  35213  sbcalf  38449  sbcexf  38450  sbccom2lem  38459  sbccom2  38460  sbccom2f  38461  sbccom2fi  38462  csbcom2fi  38463  rspcsbnea  42584  2sbcrex  43230  2sbcrexOLD  43232  sbcrot3  43237  sbcrot5  43238  2rexfrabdioph  43242  3rexfrabdioph  43243  4rexfrabdioph  43244  6rexfrabdioph  43245  7rexfrabdioph  43246  rmydioph  43460  expdiophlem2  43468  sbcheg  44224  sbc3or  44977  trsbc  44985  onfrALTlem5  44987  eqsbc2VD  45284  sbcoreleleqVD  45303  onfrALTlem5VD  45329  ich2exprop  47943