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

Theorem ralcom2 2941
 Description: Commutation of restricted universal quantifiers. Note that and need not be distinct (this makes the proof longer). (Contributed by NM, 24-Nov-1994.) (Proof shortened by Mario Carneiro, 17-Oct-2016.)
Assertion
Ref Expression
ralcom2
Distinct variable groups:   ,   ,
Allowed substitution hints:   (,)

Proof of Theorem ralcom2
StepHypRef Expression
1 eleq1 2537 . . . . . . 7
21sps 1963 . . . . . 6
32imbi1d 324 . . . . . . . . 9
43dral1 2174 . . . . . . . 8
54bicomd 206 . . . . . . 7
6 df-ral 2761 . . . . . . 7
7 df-ral 2761 . . . . . . 7
85, 6, 73bitr4g 296 . . . . . 6
92, 8imbi12d 327 . . . . 5
109dral1 2174 . . . 4
11 df-ral 2761 . . . 4
12 df-ral 2761 . . . 4
1310, 11, 123bitr4g 296 . . 3
1413biimpd 212 . 2
15 nfnae 2167 . . . . 5
16 nfra2 2790 . . . . 5
1715, 16nfan 2031 . . . 4
18 nfnae 2167 . . . . . . . 8
19 nfra1 2785 . . . . . . . 8
2018, 19nfan 2031 . . . . . . 7
21 nfcvf 2635 . . . . . . . . 9
2221adantr 472 . . . . . . . 8
23 nfcvd 2613 . . . . . . . 8
2422, 23nfeld 2620 . . . . . . 7
2520, 24nfan1 2030 . . . . . 6
26 rsp2 2780 . . . . . . . . 9
2726ancomsd 461 . . . . . . . 8
2827expdimp 444 . . . . . . 7
2928adantll 728 . . . . . 6
3025, 29ralrimi 2800 . . . . 5
3130ex 441 . . . 4
3217, 31ralrimi 2800 . . 3
3332ex 441 . 2
3414, 33pm2.61i 169 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wa 376  wal 1450   wcel 1904  wnfc 2599  wral 2756 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451 This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ral 2761 This theorem is referenced by:  tz7.48lem  7176  imo72b2  36689  tratrb  36967  tratrbVD  37321
 Copyright terms: Public domain W3C validator