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

Theorem ralcom4 3128
Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
Assertion
Ref Expression
ralcom4
Distinct variable groups:   ,   ,

Proof of Theorem ralcom4
StepHypRef Expression
1 ralcom 3018 . 2
2 ralv 3123 . . 3
32ralbii 2888 . 2
4 ralv 3123 . 2
51, 3, 43bitr3i 275 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  A.wal 1393  A.wral 2807   cvv 3109
This theorem is referenced by:  ralxpxfr2d  3224  uniiunlem  3587  iunss  4371  disjor  4436  trint  4560  reliun  5128  funimass4  5924  ralrnmpt2  6417  findcard3  7783  kmlem12  8562  fimaxre3  10517  vdwmc2  14497  ramtlecl  14518  iunocv  18712  1stccn  19964  itg2leub  22141  mptelee  24198  nmoubi  25687  nmopub  26827  nmfnleub  26844  moel  27382  disjorf  27440  funcnv5mpt  27511  untuni  29081  heibor1lem  30305  pmapglbx  35493
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-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  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-nfc 2607  df-ral 2812  df-v 3111
  Copyright terms: Public domain W3C validator