Theorem sbcbii 3802

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

Syntax hints:   ↔ wb 205  ⊤wtru 1542  [wsbc 3742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-sbc 3743

This theorem is referenced by:  eqsbc2  3811  sbc3an  3812  sbccomlem  3829  sbccom  3830  sbcrext  3832  sbcabel  3837  csbcow  3873  csbco  3874  sbcnel12g  4376  sbcne12  4377  csbcom  4382  csbnestgfw  4384  csbnestgf  4389  sbccsb  4398  sbccsb2  4399  csbab  4402  2nreu  4406  sbcssg  4486  sbcop  5451  sbcrel  5741  difopabOLD  5792  sbcfung  6530  tfinds2  7805  frpoins3xpg  8077  frpoins3xp3g  8078  mpoxopovel  8156  f1od2  31706  bnj62  33421  bnj89  33422  bnj156  33429  bnj524  33438  bnj610  33448  bnj919  33468  bnj976  33478  bnj110  33559  bnj91  33562  bnj92  33563  bnj106  33569  bnj121  33571  bnj124  33572  bnj125  33573  bnj126  33574  bnj130  33575  bnj154  33579  bnj155  33580  bnj153  33581  bnj207  33582  bnj523  33588  bnj526  33589  bnj539  33592  bnj540  33593  bnj581  33609  bnj591  33612  bnj609  33618  bnj611  33619  bnj934  33636  bnj1000  33642  bnj984  33653  bnj985v  33654  bnj985  33655  bnj1040  33673  bnj1123  33687  bnj1452  33753  bnj1463  33756  sbcalf  36646  sbcexf  36647  sbccom2lem  36656  sbccom2  36657  sbccom2f  36658  sbccom2fi  36659  csbcom2fi  36660  2sbcrex  41165  2sbcrexOLD  41167  sbcrot3  41172  sbcrot5  41173  2rexfrabdioph  41177  3rexfrabdioph  41178  4rexfrabdioph  41179  6rexfrabdioph  41180  7rexfrabdioph  41181  rmydioph  41396  expdiophlem2  41404  sbcheg  42173  sbc3or  42936  trsbc  42944  onfrALTlem5  42946  eqsbc2VD  43244  sbcoreleleqVD  43263  onfrALTlem5VD  43289  ich2exprop  45783