Theorem sbcbii 3801

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

Syntax hints:   ↔ wb 206  ⊤wtru 1541  [wsbc 3744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3745

This theorem is referenced by:  eqsbc2  3808  sbc3an  3809  sbccomlemOLD  3824  sbccom  3825  sbcrext  3827  sbcabel  3832  csbcow  3868  csbco  3869  sbcnel12g  4367  sbcne12  4368  csbcom  4373  csbnestgfw  4375  csbnestgf  4380  sbccsb  4389  sbccsb2  4390  csbab  4393  2nreu  4397  sbcssg  4473  sbcop  5436  sbcrel  5728  sbcfung  6510  tfinds2  7804  frpoins3xpg  8080  frpoins3xp3g  8081  mpoxopovel  8160  f1od2  32677  bnj62  34689  bnj89  34690  bnj156  34697  bnj524  34706  bnj610  34716  bnj919  34736  bnj976  34746  bnj110  34827  bnj91  34830  bnj92  34831  bnj106  34837  bnj121  34839  bnj124  34840  bnj125  34841  bnj126  34842  bnj130  34843  bnj154  34847  bnj155  34848  bnj153  34849  bnj207  34850  bnj523  34856  bnj526  34857  bnj539  34860  bnj540  34861  bnj581  34877  bnj591  34880  bnj609  34886  bnj611  34887  bnj934  34904  bnj1000  34910  bnj984  34921  bnj985v  34922  bnj985  34923  bnj1040  34941  bnj1123  34955  bnj1452  35021  bnj1463  35024  sbcalf  38096  sbcexf  38097  sbccom2lem  38106  sbccom2  38107  sbccom2f  38108  sbccom2fi  38109  csbcom2fi  38110  rspcsbnea  42107  2sbcrex  42760  2sbcrexOLD  42762  sbcrot3  42767  sbcrot5  42768  2rexfrabdioph  42772  3rexfrabdioph  42773  4rexfrabdioph  42774  6rexfrabdioph  42775  7rexfrabdioph  42776  rmydioph  42990  expdiophlem2  42998  sbcheg  43755  sbc3or  44509  trsbc  44517  onfrALTlem5  44519  eqsbc2VD  44816  sbcoreleleqVD  44835  onfrALTlem5VD  44861  ich2exprop  47459