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

Theorem ralunb 3777
Description: Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Assertion
Ref Expression
ralunb (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑))

Proof of Theorem ralunb
StepHypRef Expression
1 elun 3736 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
21imbi1i 339 . . . . 5 ((𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ((𝑥𝐴𝑥𝐵) → 𝜑))
3 jaob 821 . . . . 5 (((𝑥𝐴𝑥𝐵) → 𝜑) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
42, 3bitri 264 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
54albii 1744 . . 3 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
6 19.26 1797 . . 3 (∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
75, 6bitri 264 . 2 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
8 df-ral 2917 . 2 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑))
9 df-ral 2917 . . 3 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
10 df-ral 2917 . . 3 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
119, 10anbi12i 732 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
127, 8, 113bitr4i 292 1 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384  wal 1478  wcel 1992  wral 2912  cun 3558
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-v 3193  df-un 3565
This theorem is referenced by:  ralun  3778  raldifeq  4036  ralprg  4210  raltpg  4212  ralunsn  4395  disjxun  4616  undifixp  7889  ixpfi2  8209  dffi3  8282  fseqenlem1  8792  hashf1lem1  13174  2swrdeqwrdeq  13386  rexfiuz  14016  modfsummods  14447  modfsummod  14448  coprmproddvdslem  15295  prmind2  15317  prmreclem2  15540  lubun  17039  efgsp1  18066  coe1fzgsumdlem  19585  evl1gsumdlem  19634  unocv  19938  basdif0  20663  isclo  20796  ordtrest2  20913  ptbasfi  21289  ptcnplem  21329  ptrescn  21347  ordthmeolem  21509  prdsxmetlem  22078  prdsbl  22201  iblcnlem1  23455  ellimc2  23542  rlimcnp  24587  xrlimcnp  24590  ftalem3  24696  dchreq  24878  2sqlem10  25048  dchrisum0flb  25094  pntpbnd1  25170  wlkp1lem8  26440  pthdlem1  26525  crctcshwlkn0lem7  26571  wwlksnext  26651  clwwlksel  26774  wwlksext2clwwlk  26784  3wlkdlem4  26882  3pthdlem1  26884  upgr4cycl4dv4e  26905  dfconngr1  26908  numclwwlkovf2ex  27069  ordtrest2NEW  29743  subfacp1lem3  30864  subfacp1lem5  30866  erdszelem8  30880  hfext  31924  finixpnum  33012  lindsenlbs  33022  poimirlem26  33053  poimirlem27  33054  poimirlem32  33059  prdsbnd  33210  rrnequiv  33252  hdmap14lem13  36638  pfxsuffeqwrdeq  40693
  Copyright terms: Public domain W3C validator