Theorem sbcbii 3829

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

Syntax hints:   ↔ wb 208  ⊤wtru 1538  [wsbc 3772

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1540  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-sbc 3773

This theorem is referenced by:  eqsbc3r  3837  sbc3an  3838  sbccomlem  3853  sbccom  3854  sbcrext  3856  sbcabel  3861  csbcow  3898  csbco  3899  sbcnel12g  4363  sbcne12  4364  csbcom  4369  csbnestgfw  4371  csbnestgf  4376  sbccsb  4385  sbccsb2  4386  csbab  4389  2nreu  4393  sbcssg  4463  sbcop  5380  sbcrel  5655  difopab  5702  sbcfung  6379  tfinds2  7578  mpoxopovel  7886  f1od2  30457  bnj62  31990  bnj89  31991  bnj156  31998  bnj524  32008  bnj610  32018  bnj919  32038  bnj976  32049  bnj110  32130  bnj91  32133  bnj92  32134  bnj106  32140  bnj121  32142  bnj124  32143  bnj125  32144  bnj126  32145  bnj130  32146  bnj154  32150  bnj155  32151  bnj153  32152  bnj207  32153  bnj523  32159  bnj526  32160  bnj539  32163  bnj540  32164  bnj581  32180  bnj591  32183  bnj609  32189  bnj611  32190  bnj934  32207  bnj1000  32213  bnj984  32224  bnj985v  32225  bnj985  32226  bnj1040  32244  bnj1123  32258  bnj1452  32324  bnj1463  32327  sbcalf  35407  sbcexf  35408  sbccom2lem  35417  sbccom2  35418  sbccom2f  35419  sbccom2fi  35420  csbcom2fi  35421  2sbcrex  39401  2sbcrexOLD  39403  sbcrot3  39408  sbcrot5  39409  2rexfrabdioph  39413  3rexfrabdioph  39414  4rexfrabdioph  39415  6rexfrabdioph  39416  7rexfrabdioph  39417  rmydioph  39631  expdiophlem2  39639  sbcheg  40145  sbc3or  40886  trsbc  40894  onfrALTlem5  40896  eqsbc3rVD  41194  sbcoreleleqVD  41213  onfrALTlem5VD  41239  ich2exprop  43653