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 1566	1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)

Syntax hints:   ↔ wb 208  ⊤wtru 1560  [wsbc 3742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3743

This theorem is referenced by:  eqsbc2  3805  sbc3an  3806  sbccomlemOLD  3821  sbccom  3822  sbcrext  3824  sbcabel  3829  csbcow  3865  csbco  3866  sbcnel12g  4365  sbcne12  4366  csbcom  4371  csbnestgfw  4373  csbnestgf  4378  sbccsb  4387  sbccsb2  4388  csbab  4391  2nreu  4395  sbcssg  4472  sbcop  5454  sbcrel  5749  sbcfung  6539  tfinds2  7838  frpoins3xpg  8113  frpoins3xp3g  8114  mpoxopovel  8193  f1od2  32881  bnj62  34976  bnj89  34977  bnj156  34984  bnj524  34993  bnj610  35003  bnj919  35023  bnj976  35033  bnj110  35113  bnj91  35116  bnj92  35117  bnj106  35123  bnj121  35125  bnj124  35126  bnj125  35127  bnj126  35128  bnj130  35129  bnj154  35133  bnj155  35134  bnj153  35135  bnj207  35136  bnj523  35142  bnj526  35143  bnj539  35146  bnj540  35147  bnj581  35163  bnj591  35166  bnj609  35172  bnj611  35173  bnj934  35190  bnj1000  35196  bnj984  35207  bnj985v  35208  bnj985  35209  bnj1040  35227  bnj1123  35241  bnj1452  35307  bnj1463  35310  sbcalf  38573  sbcexf  38574  sbccom2lem  38583  sbccom2  38584  sbccom2f  38585  sbccom2fi  38586  csbcom2fi  38587  rspcsbnea  42708  2sbcrex  43325  sbcrot3  43328  sbcrot5  43329  2rexfrabdioph  43333  3rexfrabdioph  43334  4rexfrabdioph  43335  6rexfrabdioph  43336  7rexfrabdioph  43337  rmydioph  43551  expdiophlem2  43559  sbcheg  44315  sbc3or  45068  trsbc  45076  onfrALTlem5  45078  eqsbc2VD  45375  sbcoreleleqVD  45394  onfrALTlem5VD  45420  ich2exprop  48037