Theorem sbcbii 3798

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

Syntax hints:   ↔ wb 206  ⊤wtru 1542  [wsbc 3741

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-sbc 3742

This theorem is referenced by:  eqsbc2  3805  sbc3an  3806  sbccomlemOLD  3821  sbccom  3822  sbcrext  3824  sbcabel  3829  csbcow  3865  csbco  3866  sbcnel12g  4364  sbcne12  4365  csbcom  4370  csbnestgfw  4372  csbnestgf  4377  sbccsb  4386  sbccsb2  4387  csbab  4390  2nreu  4394  sbcssg  4470  sbcop  5429  sbcrel  5721  sbcfung  6505  tfinds2  7794  frpoins3xpg  8070  frpoins3xp3g  8071  mpoxopovel  8150  f1od2  32700  bnj62  34730  bnj89  34731  bnj156  34738  bnj524  34747  bnj610  34757  bnj919  34777  bnj976  34787  bnj110  34868  bnj91  34871  bnj92  34872  bnj106  34878  bnj121  34880  bnj124  34881  bnj125  34882  bnj126  34883  bnj130  34884  bnj154  34888  bnj155  34889  bnj153  34890  bnj207  34891  bnj523  34897  bnj526  34898  bnj539  34901  bnj540  34902  bnj581  34918  bnj591  34921  bnj609  34927  bnj611  34928  bnj934  34945  bnj1000  34951  bnj984  34962  bnj985v  34963  bnj985  34964  bnj1040  34982  bnj1123  34996  bnj1452  35062  bnj1463  35065  sbcalf  38160  sbcexf  38161  sbccom2lem  38170  sbccom2  38171  sbccom2f  38172  sbccom2fi  38173  csbcom2fi  38174  rspcsbnea  42170  2sbcrex  42823  2sbcrexOLD  42825  sbcrot3  42830  sbcrot5  42831  2rexfrabdioph  42835  3rexfrabdioph  42836  4rexfrabdioph  42837  6rexfrabdioph  42838  7rexfrabdioph  42839  rmydioph  43053  expdiophlem2  43061  sbcheg  43818  sbc3or  44571  trsbc  44579  onfrALTlem5  44581  eqsbc2VD  44878  sbcoreleleqVD  44897  onfrALTlem5VD  44923  ich2exprop  47508