Theorem sbcbii 3851

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

Syntax hints:   ↔ wb 206  ⊤wtru 1537  [wsbc 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-sbc 3791

This theorem is referenced by:  eqsbc2  3859  sbc3an  3860  sbccomlemOLD  3878  sbccom  3879  sbcrext  3881  sbcabel  3886  csbcow  3922  csbco  3923  sbcnel12g  4419  sbcne12  4420  csbcom  4425  csbnestgfw  4427  csbnestgf  4432  sbccsb  4441  sbccsb2  4442  csbab  4445  2nreu  4449  sbcssg  4525  sbcop  5499  sbcrel  5792  difopabOLD  5843  sbcfung  6591  tfinds2  7884  frpoins3xpg  8163  frpoins3xp3g  8164  mpoxopovel  8243  f1od2  32738  bnj62  34712  bnj89  34713  bnj156  34720  bnj524  34729  bnj610  34739  bnj919  34759  bnj976  34769  bnj110  34850  bnj91  34853  bnj92  34854  bnj106  34860  bnj121  34862  bnj124  34863  bnj125  34864  bnj126  34865  bnj130  34866  bnj154  34870  bnj155  34871  bnj153  34872  bnj207  34873  bnj523  34879  bnj526  34880  bnj539  34883  bnj540  34884  bnj581  34900  bnj591  34903  bnj609  34909  bnj611  34910  bnj934  34927  bnj1000  34933  bnj984  34944  bnj985v  34945  bnj985  34946  bnj1040  34964  bnj1123  34978  bnj1452  35044  bnj1463  35047  sbcalf  38100  sbcexf  38101  sbccom2lem  38110  sbccom2  38111  sbccom2f  38112  sbccom2fi  38113  csbcom2fi  38114  rspcsbnea  42112  2sbcrex  42771  2sbcrexOLD  42773  sbcrot3  42778  sbcrot5  42779  2rexfrabdioph  42783  3rexfrabdioph  42784  4rexfrabdioph  42785  6rexfrabdioph  42786  7rexfrabdioph  42787  rmydioph  43002  expdiophlem2  43010  sbcheg  43768  sbc3or  44529  trsbc  44537  onfrALTlem5  44539  eqsbc2VD  44837  sbcoreleleqVD  44856  onfrALTlem5VD  44882  ich2exprop  47395