Theorem sbcbii 3846

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789

This theorem is referenced by:  eqsbc2  3854  sbc3an  3855  sbccomlemOLD  3870  sbccom  3871  sbcrext  3873  sbcabel  3878  csbcow  3914  csbco  3915  sbcnel12g  4414  sbcne12  4415  csbcom  4420  csbnestgfw  4422  csbnestgf  4427  sbccsb  4436  sbccsb2  4437  csbab  4440  2nreu  4444  sbcssg  4520  sbcop  5494  sbcrel  5790  difopabOLD  5841  sbcfung  6590  tfinds2  7885  frpoins3xpg  8165  frpoins3xp3g  8166  mpoxopovel  8245  f1od2  32732  bnj62  34734  bnj89  34735  bnj156  34742  bnj524  34751  bnj610  34761  bnj919  34781  bnj976  34791  bnj110  34872  bnj91  34875  bnj92  34876  bnj106  34882  bnj121  34884  bnj124  34885  bnj125  34886  bnj126  34887  bnj130  34888  bnj154  34892  bnj155  34893  bnj153  34894  bnj207  34895  bnj523  34901  bnj526  34902  bnj539  34905  bnj540  34906  bnj581  34922  bnj591  34925  bnj609  34931  bnj611  34932  bnj934  34949  bnj1000  34955  bnj984  34966  bnj985v  34967  bnj985  34968  bnj1040  34986  bnj1123  35000  bnj1452  35066  bnj1463  35069  sbcalf  38121  sbcexf  38122  sbccom2lem  38131  sbccom2  38132  sbccom2f  38133  sbccom2fi  38134  csbcom2fi  38135  rspcsbnea  42132  2sbcrex  42795  2sbcrexOLD  42797  sbcrot3  42802  sbcrot5  42803  2rexfrabdioph  42807  3rexfrabdioph  42808  4rexfrabdioph  42809  6rexfrabdioph  42810  7rexfrabdioph  42811  rmydioph  43026  expdiophlem2  43034  sbcheg  43792  sbc3or  44552  trsbc  44560  onfrALTlem5  44562  eqsbc2VD  44860  sbcoreleleqVD  44879  onfrALTlem5VD  44905  ich2exprop  47458