Theorem sbcbii 3798

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

This proof depends on syntax axioms:   ↔ wb 209  ⊤wtru 1571  [wsbc 3742

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3743

This theorem is used by:  eqsbc2  3805  sbc3an  3806  sbccom  3821  sbcrext  3823  sbcabel  3828  csbcow  3865  csbco  3866  sbcnel12g  4375  sbcne12  4376  csbcom  4381  csbnestgfw  4383  csbnestgf  4388  sbccsb  4397  sbccsb2  4398  csbab  4401  2nreu  4405  sbcssg  4480  sbcop  5469  sbcrel  5765  sbcfung  6561  tfinds2  7864  frpoins3xpg  8142  frpoins3xp3g  8143  mpoxopovel  8222  f1od2  33198  bnj62  35238  bnj89  35239  bnj156  35246  bnj524  35255  bnj610  35265  bnj919  35285  bnj976  35295  bnj110  35375  bnj91  35378  bnj92  35379  bnj106  35385  bnj121  35387  bnj124  35388  bnj125  35389  bnj126  35390  bnj130  35391  bnj154  35395  bnj155  35396  bnj153  35397  bnj207  35398  bnj523  35404  bnj526  35405  bnj539  35408  bnj540  35409  bnj581  35425  bnj591  35428  bnj609  35434  bnj611  35435  bnj934  35452  bnj1000  35458  bnj984  35469  bnj985v  35470  bnj985  35471  bnj1040  35489  bnj1123  35503  bnj1452  35569  bnj1463  35572  sbcalf  38870  sbcexf  38871  sbccom2lem  38880  sbccom2  38881  sbccom2f  38882  sbccom2fi  38883  csbcom2fi  38884  rspcsbnea  43005  2sbcrex  43637  sbcrot3  43640  sbcrot5  43641  2rexfrabdioph  43645  3rexfrabdioph  43646  4rexfrabdioph  43647  6rexfrabdioph  43648  7rexfrabdioph  43649  rmydioph  43863  expdiophlem2  43871  sbcheg  44627  sbc3or  45363  trsbc  45371  onfrALTlem5  45373  eqsbc2VD  45670  sbcoreleleqVD  45689  onfrALTlem5VD  45715  ich2exprop  48379