Theorem sbcbii 3795

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

Syntax hints:   ↔ wb 208  ⊤wtru 1555  [wsbc 3739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1557  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-sbc 3740

This theorem is referenced by:  eqsbc2  3802  sbc3an  3803  sbccomlemOLD  3818  sbccom  3819  sbcrext  3821  sbcabel  3826  csbcow  3862  csbco  3863  sbcnel12g  4362  sbcne12  4363  csbcom  4368  csbnestgfw  4370  csbnestgf  4375  sbccsb  4384  sbccsb2  4385  csbab  4388  2nreu  4392  sbcssg  4469  sbcop  5451  sbcrel  5746  sbcfung  6534  tfinds2  7833  frpoins3xpg  8108  frpoins3xp3g  8109  mpoxopovel  8188  f1od2  32864  bnj62  34973  bnj89  34974  bnj156  34981  bnj524  34990  bnj610  35000  bnj919  35020  bnj976  35030  bnj110  35110  bnj91  35113  bnj92  35114  bnj106  35120  bnj121  35122  bnj124  35123  bnj125  35124  bnj126  35125  bnj130  35126  bnj154  35130  bnj155  35131  bnj153  35132  bnj207  35133  bnj523  35139  bnj526  35140  bnj539  35143  bnj540  35144  bnj581  35160  bnj591  35163  bnj609  35169  bnj611  35170  bnj934  35187  bnj1000  35193  bnj984  35204  bnj985v  35205  bnj985  35206  bnj1040  35224  bnj1123  35238  bnj1452  35304  bnj1463  35307  sbcalf  38561  sbcexf  38562  sbccom2lem  38571  sbccom2  38572  sbccom2f  38573  sbccom2fi  38574  csbcom2fi  38575  rspcsbnea  42696  2sbcrex  43313  sbcrot3  43316  sbcrot5  43317  2rexfrabdioph  43321  3rexfrabdioph  43322  4rexfrabdioph  43323  6rexfrabdioph  43324  7rexfrabdioph  43325  rmydioph  43539  expdiophlem2  43547  sbcheg  44303  sbc3or  45056  trsbc  45064  onfrALTlem5  45066  eqsbc2VD  45363  sbcoreleleqVD  45382  onfrALTlem5VD  45408  ich2exprop  48025