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

Theorem sb8iota 5242
 Description: Variable substitution in description binder. Compare sb8eu 2174. (Contributed by NM, 18-Mar-2013.)
Hypothesis
Ref Expression
sb8iota.1
Assertion
Ref Expression
sb8iota

Proof of Theorem sb8iota
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1609 . . . . . 6
21sb8 2045 . . . . 5
3 sbbi 2024 . . . . . . 7
4 sb8iota.1 . . . . . . . . 9
54nfsb 2061 . . . . . . . 8
6 eqsb3 2397 . . . . . . . . 9
7 nfv 1609 . . . . . . . . 9
86, 7nfxfr 1560 . . . . . . . 8
95, 8nfbi 1784 . . . . . . 7
103, 9nfxfr 1560 . . . . . 6
11 nfv 1609 . . . . . 6
12 sbequ 2013 . . . . . 6
1310, 11, 12cbval 1937 . . . . 5
14 equsb3 2054 . . . . . . 7
1514sblbis 2025 . . . . . 6
1615albii 1556 . . . . 5
172, 13, 163bitri 262 . . . 4
1817abbii 2408 . . 3
1918unieqi 3853 . 2
20 dfiota2 5236 . 2
21 dfiota2 5236 . 2
2219, 20, 213eqtr4i 2326 1
 Colors of variables: wff set class Syntax hints:   wb 176  wal 1530  wnf 1534   wceq 1632  wsb 1638  cab 2282  cuni 3843  cio 5233 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-sn 3659  df-uni 3844  df-iota 5235
 Copyright terms: Public domain W3C validator