Theorem sbcbii 3838

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

Syntax hints:   ↔ wb 205  ⊤wtru 1543  [wsbc 3778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3779

This theorem is referenced by:  eqsbc2  3847  sbc3an  3848  sbccomlem  3865  sbccom  3866  sbcrext  3868  sbcabel  3873  csbcow  3909  csbco  3910  sbcnel12g  4412  sbcne12  4413  csbcom  4418  csbnestgfw  4420  csbnestgf  4425  sbccsb  4434  sbccsb2  4435  csbab  4438  2nreu  4442  sbcssg  4524  sbcop  5490  sbcrel  5781  difopabOLD  5832  sbcfung  6573  tfinds2  7853  frpoins3xpg  8126  frpoins3xp3g  8127  mpoxopovel  8205  f1od2  31946  bnj62  33731  bnj89  33732  bnj156  33739  bnj524  33748  bnj610  33758  bnj919  33778  bnj976  33788  bnj110  33869  bnj91  33872  bnj92  33873  bnj106  33879  bnj121  33881  bnj124  33882  bnj125  33883  bnj126  33884  bnj130  33885  bnj154  33889  bnj155  33890  bnj153  33891  bnj207  33892  bnj523  33898  bnj526  33899  bnj539  33902  bnj540  33903  bnj581  33919  bnj591  33922  bnj609  33928  bnj611  33929  bnj934  33946  bnj1000  33952  bnj984  33963  bnj985v  33964  bnj985  33965  bnj1040  33983  bnj1123  33997  bnj1452  34063  bnj1463  34066  sbcalf  36982  sbcexf  36983  sbccom2lem  36992  sbccom2  36993  sbccom2f  36994  sbccom2fi  36995  csbcom2fi  36996  2sbcrex  41522  2sbcrexOLD  41524  sbcrot3  41529  sbcrot5  41530  2rexfrabdioph  41534  3rexfrabdioph  41535  4rexfrabdioph  41536  6rexfrabdioph  41537  7rexfrabdioph  41538  rmydioph  41753  expdiophlem2  41761  sbcheg  42530  sbc3or  43293  trsbc  43301  onfrALTlem5  43303  eqsbc2VD  43601  sbcoreleleqVD  43620  onfrALTlem5VD  43646  ich2exprop  46139