Theorem ralrimivva 2552

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.)

Hypothesis

Ref	Expression
ralrimivva.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓)

Assertion

Ref	Expression
ralrimivva	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Distinct variable groups:   𝜑,𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem ralrimivva

Step	Hyp	Ref	Expression
1		ralrimivva.1	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓)
2	1	ex 114	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓))
3	2	ralrimivv 2551	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2141  ∀wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453

This theorem is referenced by:  swopo  4291  sosng  4684  fcof1  5762  fliftfund  5776  isoresbr  5788  isocnv  5790  f1oiso  5805  oveqrspc2v  5880  caovclg  6005  caovcomg  6008  off  6073  caofrss  6085  oprssdmm  6150  dmmpog  6188  fnmpoovd  6194  fmpoco  6195  poxp  6211  f1od2  6214  eroprf  6606  dom2lem  6750  xpf1o  6822  fidifsnid  6849  nnwetri  6893  undiffi  6902  fidcenumlemim  6929  supmoti  6970  supsnti  6982  supisoti  6987  difinfsnlem  7076  nninfwlpor  7150  cc2lem  7228  addlocpr  7498  mullocpr  7533  cauappcvgprlemloc  7614  cauappcvgprlemlim  7623  caucvgprlemloc  7637  caucvgprprlemloc  7665  suplocexprlemloc  7683  suplocsrlemb  7768  rereceu  7851  axpre-suploclemres  7863  ltordlem  8401  cju  8877  exbtwnz  10207  frec2uzf1od  10362  frec2uzisod  10363  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgsuc  10370  frecuzrdgrclt  10371  frecuzrdgg  10372  frecuzrdgsuctlem  10379  seqvalcd  10415  seqovcd  10419  seq3caopr3  10437  seq3caopr2  10438  iseqf1olemqf1o  10449  seq3homo  10466  seq3distr  10469  fimaxq  10762  zfz1isolem1  10775  rsqrmo  10991  climcn2  11272  addcn2  11273  mulcn2  11275  fsum2dlemstep  11397  fisumcom2  11401  cvgratnn  11494  fprodcl2lem  11568  fprod2dlemstep  11585  fprodcom2fi  11589  divalglemeunn  11880  divalglemeuneg  11882  bezoutlemeu  11962  isprm6  12101  pw2dvdseu  12122  crth  12178  eulerthlemh  12185  ennnfonelemim  12379  nninfdclemf1  12407  unbendc  12409  plusffng  12619  mgmplusf  12620  opifismgmdc  12625  ismndd  12673  mndpropd  12676  mndinvmod  12678  mhmpropd  12689  idmhm  12692  mhmf1o  12693  issubmd  12696  mndissubm  12697  submid  12699  0mhm  12704  mhmco  12705  grppropd  12724  tgclb  12859  txbas  13052  txcnp  13065  txcnmpt  13067  cnmpt21  13085  txswaphmeo  13115  isxmetd  13141  isxmet2d  13142  xmettpos  13164  blfvalps  13179  xmetresbl  13234  metss2  13292  comet  13293  bdmet  13296  bdmopn  13298  xmetxp  13301  qtopbasss  13315  elcncf1di  13360  cncffvrn  13363  mulc1cncf  13370  cncfco  13372  dedekindeulemloc  13391  dedekindeu  13395  dedekindicclemloc  13400  dedekindicclemicc  13404  ivthinclemloc  13413  sssneq  14035  exmidsbthrlem  14054  cvgcmp2n  14065  trirec0  14076  apdiff  14080  redc0  14089  reap0  14090