Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbc5 Unicode version

Theorem sbc5 3352
 Description: An equivalence for class substitution. (Contributed by NM, 23-Aug-1993.) (Revised by Mario Carneiro, 12-Oct-2016.)
Assertion
Ref Expression
sbc5
Distinct variable group:   ,

Proof of Theorem sbc5
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 sbcex 3337 . 2
2 exsimpl 1677 . . 3
3 isset 3113 . . 3
42, 3sylibr 212 . 2
5 dfsbcq2 3330 . . 3
6 eqeq2 2472 . . . . 5
76anbi1d 704 . . . 4
87exbidv 1714 . . 3
9 sb5 2174 . . 3
105, 8, 9vtoclbg 3168 . 2
111, 4, 10pm5.21nii 353 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  /\wa 369  =wceq 1395  E.wex 1612  [wsb 1739  e.wcel 1818   cvv 3109  [.wsbc 3327 This theorem is referenced by:  sbc6g  3353  sbc7  3355  sbciegft  3358  sbccomlem  3406  csb2  3436  rexsns  4062  rexsnsOLD  4063  sbccom2lem  30529  pm13.192  31317  pm13.195  31320  2sbc5g  31323  iotasbc  31326  pm14.122b  31330  iotasbc5  31338 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-sbc 3328
 Copyright terms: Public domain W3C validator