Theorem sbcbii 3803

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

Syntax hints:   ↔ wb 209  ⊤wtru 1564  [wsbc 3747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-sbc 3748

This theorem is referenced by:  eqsbc2  3810  sbc3an  3811  sbccomlemOLD  3826  sbccom  3827  sbcrext  3829  sbcabel  3834  csbcow  3870  csbco  3871  sbcnel12g  4371  sbcne12  4372  csbcom  4377  csbnestgfw  4379  csbnestgf  4384  sbccsb  4393  sbccsb2  4394  csbab  4397  2nreu  4401  sbcssg  4478  sbcop  5461  sbcrel  5757  sbcfung  6549  tfinds2  7848  frpoins3xpg  8124  frpoins3xp3g  8125  mpoxopovel  8204  f1od2  32972  bnj62  35021  bnj89  35022  bnj156  35029  bnj524  35038  bnj610  35048  bnj919  35068  bnj976  35078  bnj110  35158  bnj91  35161  bnj92  35162  bnj106  35168  bnj121  35170  bnj124  35171  bnj125  35172  bnj126  35173  bnj130  35174  bnj154  35178  bnj155  35179  bnj153  35180  bnj207  35181  bnj523  35187  bnj526  35188  bnj539  35191  bnj540  35192  bnj581  35208  bnj591  35211  bnj609  35217  bnj611  35218  bnj934  35235  bnj1000  35241  bnj984  35252  bnj985v  35253  bnj985  35254  bnj1040  35272  bnj1123  35286  bnj1452  35352  bnj1463  35355  sbcalf  38620  sbcexf  38621  sbccom2lem  38630  sbccom2  38631  sbccom2f  38632  sbccom2fi  38633  csbcom2fi  38634  rspcsbnea  42755  2sbcrex  43372  sbcrot3  43375  sbcrot5  43376  2rexfrabdioph  43380  3rexfrabdioph  43381  4rexfrabdioph  43382  6rexfrabdioph  43383  7rexfrabdioph  43384  rmydioph  43598  expdiophlem2  43606  sbcheg  44362  sbc3or  45100  trsbc  45108  onfrALTlem5  45110  eqsbc2VD  45407  sbcoreleleqVD  45426  onfrALTlem5VD  45452  ich2exprop  48076