Theorem sbcbii 3754

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

Syntax hints:   ↔ wb 209  ⊤wtru 1540  [wsbc 3697

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-sbc 3698

This theorem is referenced by:  eqsbc3r  3762  sbc3an  3763  sbccomlem  3777  sbccom  3778  sbcrext  3780  sbcabel  3785  csbcow  3821  csbco  3822  sbcnel12g  4309  sbcne12  4310  csbcom  4315  csbnestgfw  4317  csbnestgf  4322  sbccsb  4331  sbccsb2  4332  csbab  4335  2nreu  4339  sbcssg  4417  sbcop  5349  sbcrel  5625  difopab  5672  sbcfung  6360  tfinds2  7578  mpoxopovel  7897  f1od2  30573  bnj62  32211  bnj89  32212  bnj156  32219  bnj524  32229  bnj610  32239  bnj919  32259  bnj976  32270  bnj110  32351  bnj91  32354  bnj92  32355  bnj106  32361  bnj121  32363  bnj124  32364  bnj125  32365  bnj126  32366  bnj130  32367  bnj154  32371  bnj155  32372  bnj153  32373  bnj207  32374  bnj523  32380  bnj526  32381  bnj539  32384  bnj540  32385  bnj581  32401  bnj591  32404  bnj609  32410  bnj611  32411  bnj934  32428  bnj1000  32434  bnj984  32445  bnj985v  32446  bnj985  32447  bnj1040  32465  bnj1123  32479  bnj1452  32545  bnj1463  32548  frpoins3xpg  33325  frpoins3xp3g  33326  sbcalf  35825  sbcexf  35826  sbccom2lem  35835  sbccom2  35836  sbccom2f  35837  sbccom2fi  35838  csbcom2fi  35839  2sbcrex  40091  2sbcrexOLD  40093  sbcrot3  40098  sbcrot5  40099  2rexfrabdioph  40103  3rexfrabdioph  40104  4rexfrabdioph  40105  6rexfrabdioph  40106  7rexfrabdioph  40107  rmydioph  40321  expdiophlem2  40329  sbcheg  40846  sbc3or  41604  trsbc  41612  onfrALTlem5  41614  eqsbc3rVD  41912  sbcoreleleqVD  41931  onfrALTlem5VD  41957  ich2exprop  44349