Theorem sbcbii 3794

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

This proof depends on syntax axioms:   ↔ wb 209  ⊤wtru 1570  [wsbc 3738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739

This theorem is used by:  eqsbc2  3801  sbc3an  3802  sbccom  3817  sbcrext  3819  sbcabel  3824  csbcow  3861  csbco  3862  sbcnel12g  4371  sbcne12  4372  csbcom  4377  csbnestgfw  4379  csbnestgf  4384  sbccsb  4393  sbccsb2  4394  csbab  4397  2nreu  4401  sbcssg  4476  sbcop  5458  sbcrel  5756  sbcfung  6564  sbcfungOLD  6565  tfinds2  7876  f1od2  8111  frpoins3xpg  8160  frpoins3xp3g  8161  mpoxopovel  8241  bnj62  35398  bnj89  35399  bnj156  35406  bnj524  35415  bnj610  35425  bnj919  35445  bnj976  35455  bnj110  35535  bnj91  35538  bnj92  35539  bnj106  35545  bnj121  35547  bnj124  35548  bnj125  35549  bnj126  35550  bnj130  35551  bnj154  35555  bnj155  35556  bnj153  35557  bnj207  35558  bnj523  35564  bnj526  35565  bnj539  35568  bnj540  35569  bnj581  35585  bnj591  35588  bnj609  35594  bnj611  35595  bnj934  35612  bnj1000  35618  bnj984  35629  bnj985v  35630  bnj985  35631  bnj1040  35649  bnj1123  35663  bnj1452  35729  bnj1463  35732  sbcalf  39140  sbcexf  39141  sbccom2lem  39150  sbccom2  39151  sbccom2f  39152  sbccom2fi  39153  csbcom2fi  39154  rspcsbnea  43275  2sbcrex  43889  sbcrot3  43892  sbcrot5  43893  2rexfrabdioph  43897  3rexfrabdioph  43898  4rexfrabdioph  43899  6rexfrabdioph  43900  7rexfrabdioph  43901  rmydioph  44115  expdiophlem2  44123  sbcheg  44873  sbc3or  45609  trsbc  45617  onfrALTlem5  45619  eqsbc2VD  45916  sbcoreleleqVD  45935  onfrALTlem5VD  45961  ich2exprop  48647