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

Theorem ralunb 3827
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 3786 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
21imbi1i 338 . . . . 5 ((𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ((𝑥𝐴𝑥𝐵) → 𝜑))
3 jaob 839 . . . . 5 (((𝑥𝐴𝑥𝐵) → 𝜑) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
42, 3bitri 264 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
54albii 1787 . . 3 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
6 19.26 1838 . . 3 (∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
75, 6bitri 264 . 2 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
8 df-ral 2946 . 2 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑))
9 df-ral 2946 . . 3 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
10 df-ral 2946 . . 3 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
119, 10anbi12i 733 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
127, 8, 113bitr4i 292 1 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383  wal 1521  wcel 2030  wral 2941  cun 3605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233  df-un 3612
This theorem is referenced by:  ralun  3828  raldifeq  4092  ralprg  4266  raltpg  4268  ralunsn  4454  disjxun  4683  undifixp  7986  ixpfi2  8305  dffi3  8378  fseqenlem1  8885  hashf1lem1  13277  2swrdeqwrdeq  13499  rexfiuz  14131  modfsummods  14569  modfsummod  14570  coprmproddvdslem  15423  prmind2  15445  prmreclem2  15668  lubun  17170  efgsp1  18196  coe1fzgsumdlem  19719  evl1gsumdlem  19768  unocv  20072  basdif0  20805  isclo  20939  ordtrest2  21056  ptbasfi  21432  ptcnplem  21472  ptrescn  21490  ordthmeolem  21652  prdsxmetlem  22220  prdsbl  22343  iblcnlem1  23599  ellimc2  23686  rlimcnp  24737  xrlimcnp  24740  ftalem3  24846  dchreq  25028  2sqlem10  25198  dchrisum0flb  25244  pntpbnd1  25320  wlkp1lem8  26633  pthdlem1  26718  crctcshwlkn0lem7  26764  wwlksnext  26856  clwwlkel  27009  clwwlkwwlksb  27018  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  clwwlknonex2lem2  27083  3wlkdlem4  27140  3pthdlem1  27142  upgr4cycl4dv4e  27163  dfconngr1  27166  clwwlkccatlem  27331  ordtrest2NEW  30097  subfacp1lem3  31290  subfacp1lem5  31292  erdszelem8  31306  ssltun1  32040  ssltun2  32041  hfext  32415  bj-raldifsn  33179  finixpnum  33524  lindsenlbs  33534  poimirlem26  33565  poimirlem27  33566  poimirlem32  33571  prdsbnd  33722  rrnequiv  33764  hdmap14lem13  37489  pfxsuffeqwrdeq  41731
  Copyright terms: Public domain W3C validator