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

Theorem ralunb 4146
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 elunant 4133 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
21albii 1820 . . 3 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
3 19.26 1871 . . 3 (∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
42, 3bitri 277 . 2 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
5 df-ral 3130 . 2 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑))
6 df-ral 3130 . . 3 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
7 df-ral 3130 . . 3 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
86, 7anbi12i 628 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
94, 5, 83bitr4i 305 1 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  wal 1535  wcel 2114  wral 3125  cun 3911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-ral 3130  df-v 3475  df-un 3918
This theorem is referenced by:  ralun  4147  raldifeq  4415  ralprgf  4606  raltpg  4610  ralunsn  4800  disjxun  5040  undifixp  8476  ixpfi2  8800  dffi3  8873  fseqenlem1  9428  hashf1lem1  13798  pfxsuffeqwrdeq  14040  rexfiuz  14687  modfsummods  15128  modfsummod  15129  coprmproddvdslem  15984  prmind2  16007  prmreclem2  16231  lubun  17712  efgsp1  18842  coe1fzgsumdlem  20445  evl1gsumdlem  20495  unocv  20800  basdif0  21537  isclo  21671  ordtrest2  21788  ptbasfi  22165  ptcnplem  22205  ptrescn  22223  ordthmeolem  22385  prdsxmetlem  22954  prdsbl  23077  iblcnlem1  24370  ellimc2  24459  rlimcnp  25530  xrlimcnp  25533  ftalem3  25639  dchreq  25821  2sqlem10  25991  dchrisum0flb  26073  pntpbnd1  26149  wlkp1lem8  27449  pthdlem1  27534  crctcshwlkn0lem7  27581  wwlksnext  27658  clwwlkccatlem  27753  clwwlkel  27810  clwwlkwwlksb  27818  wwlksext2clwwlk  27821  clwwlknonex2lem2  27872  3wlkdlem4  27926  3pthdlem1  27928  upgr4cycl4dv4e  27949  dfconngr1  27952  cntzun  30703  ordtrest2NEW  31174  subfacp1lem3  32437  subfacp1lem5  32439  erdszelem8  32453  ssltun1  33277  ssltun2  33278  hfext  33652  bj-raldifsn  34409  finixpnum  34918  lindsadd  34926  lindsenlbs  34928  poimirlem26  34959  poimirlem27  34960  poimirlem32  34965  prdsbnd  35107  rrnequiv  35149  hdmap14lem13  39052
  Copyright terms: Public domain W3C validator