Theorem sbcbii 3654

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

Syntax hints:   ↔ wb 197  ⊤wtru 1653  [wsbc 3598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-sbc 3599

This theorem is referenced by:  eqsbc3r  3655  sbc3an  3656  sbccomlem  3669  sbccom  3670  sbcrext  3672  sbcabel  3677  csbco  3703  sbcnel12g  4148  sbcne12  4149  csbcom  4157  csbnestgf  4159  sbccsb  4168  sbccsb2  4169  csbab  4172  sbcssg  4244  sbcrel  5377  difopab  5424  sbcfung  6094  tfinds2  7263  mpt2xopovel  7551  f1od2  29951  bnj62  31240  bnj89  31241  bnj156  31248  bnj524  31258  bnj610  31268  bnj919  31288  bnj976  31299  bnj110  31379  bnj91  31382  bnj92  31383  bnj106  31389  bnj121  31391  bnj124  31392  bnj125  31393  bnj126  31394  bnj130  31395  bnj154  31399  bnj155  31400  bnj153  31401  bnj207  31402  bnj523  31408  bnj526  31409  bnj539  31412  bnj540  31413  bnj581  31429  bnj591  31432  bnj609  31438  bnj611  31439  bnj934  31456  bnj1000  31462  bnj984  31473  bnj985  31474  bnj1040  31491  bnj1123  31505  bnj1452  31571  bnj1463  31574  sbcalf  34342  sbcexf  34343  sbccom2lem  34353  sbccom2  34354  sbccom2f  34355  sbccom2fi  34356  csbcom2fi  34358  2sbcrex  38029  2sbcrexOLD  38031  sbcrot3  38036  sbcrot5  38037  2rexfrabdioph  38041  3rexfrabdioph  38042  4rexfrabdioph  38043  6rexfrabdioph  38044  7rexfrabdioph  38045  rmydioph  38261  expdiophlem2  38269  sbcheg  38750  sbc3or  39413  trsbc  39421  onfrALTlem5  39423  eqsbc3rVD  39731  sbcoreleleqVD  39750  onfrALTlem5VD  39776