Theorem sbcbii 3777

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

Syntax hints:   ↔ wb 205  ⊤wtru 1540  [wsbc 3717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-sbc 3718

This theorem is referenced by:  eqsbc2  3786  sbc3an  3787  sbccomlem  3804  sbccom  3805  sbcrext  3807  sbcabel  3812  csbcow  3848  csbco  3849  sbcnel12g  4346  sbcne12  4347  csbcom  4352  csbnestgfw  4354  csbnestgf  4359  sbccsb  4368  sbccsb2  4369  csbab  4372  2nreu  4376  sbcssg  4455  sbcop  5404  sbcrel  5692  difopabOLD  5743  sbcfung  6465  tfinds2  7719  mpoxopovel  8045  f1od2  31065  bnj62  32708  bnj89  32709  bnj156  32716  bnj524  32726  bnj610  32736  bnj919  32756  bnj976  32766  bnj110  32847  bnj91  32850  bnj92  32851  bnj106  32857  bnj121  32859  bnj124  32860  bnj125  32861  bnj126  32862  bnj130  32863  bnj154  32867  bnj155  32868  bnj153  32869  bnj207  32870  bnj523  32876  bnj526  32877  bnj539  32880  bnj540  32881  bnj581  32897  bnj591  32900  bnj609  32906  bnj611  32907  bnj934  32924  bnj1000  32930  bnj984  32941  bnj985v  32942  bnj985  32943  bnj1040  32961  bnj1123  32975  bnj1452  33041  bnj1463  33044  frpoins3xpg  33796  frpoins3xp3g  33797  sbcalf  36281  sbcexf  36282  sbccom2lem  36291  sbccom2  36292  sbccom2f  36293  sbccom2fi  36294  csbcom2fi  36295  2sbcrex  40613  2sbcrexOLD  40615  sbcrot3  40620  sbcrot5  40621  2rexfrabdioph  40625  3rexfrabdioph  40626  4rexfrabdioph  40627  6rexfrabdioph  40628  7rexfrabdioph  40629  rmydioph  40843  expdiophlem2  40851  sbcheg  41394  sbc3or  42159  trsbc  42167  onfrALTlem5  42169  eqsbc2VD  42467  sbcoreleleqVD  42486  onfrALTlem5VD  42512  ich2exprop  44934