Theorem sbcbii 3791

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

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

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 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-sbc 3732

This theorem is referenced by:  eqsbc2  3800  sbc3an  3801  sbccomlem  3818  sbccom  3819  sbcrext  3821  sbcabel  3826  csbcow  3862  csbco  3863  sbcnel12g  4363  sbcne12  4364  csbcom  4369  csbnestgfw  4371  csbnestgf  4376  sbccsb  4385  sbccsb2  4386  csbab  4389  2nreu  4393  sbcssg  4473  sbcop  5438  sbcrel  5727  difopabOLD  5778  sbcfung  6513  tfinds2  7783  mpoxopovel  8111  f1od2  31341  bnj62  32997  bnj89  32998  bnj156  33005  bnj524  33014  bnj610  33024  bnj919  33044  bnj976  33054  bnj110  33135  bnj91  33138  bnj92  33139  bnj106  33145  bnj121  33147  bnj124  33148  bnj125  33149  bnj126  33150  bnj130  33151  bnj154  33155  bnj155  33156  bnj153  33157  bnj207  33158  bnj523  33164  bnj526  33165  bnj539  33168  bnj540  33169  bnj581  33185  bnj591  33188  bnj609  33194  bnj611  33195  bnj934  33212  bnj1000  33218  bnj984  33229  bnj985v  33230  bnj985  33231  bnj1040  33249  bnj1123  33263  bnj1452  33329  bnj1463  33332  frpoins3xpg  34069  frpoins3xp3g  34070  sbcalf  36426  sbcexf  36427  sbccom2lem  36436  sbccom2  36437  sbccom2f  36438  sbccom2fi  36439  csbcom2fi  36440  2sbcrex  40917  2sbcrexOLD  40919  sbcrot3  40924  sbcrot5  40925  2rexfrabdioph  40929  3rexfrabdioph  40930  4rexfrabdioph  40931  6rexfrabdioph  40932  7rexfrabdioph  40933  rmydioph  41148  expdiophlem2  41156  sbcheg  41758  sbc3or  42523  trsbc  42531  onfrALTlem5  42533  eqsbc2VD  42831  sbcoreleleqVD  42850  onfrALTlem5VD  42876  ich2exprop  45339