Theorem r19.21aivv 2183

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.)

Hypothesis

Ref	Expression
r19.21aivv.1	|- (ph -> ((x e. A /\ y e. B) -> ps))

Assertion

Ref	Expression
r19.21aivv	|- (ph -> A.x e. A A.y e. B ps)

Distinct variable groups:   x,y,ph   y,A

Proof of Theorem r19.21aivv

Step	Hyp	Ref	Expression
1		r19.21aivv.1	. . . 4 |- (ph -> ((x e. A /\ y e. B) -> ps))
2	1	exp3a 405	. . 3 |- (ph -> (x e. A -> (y e. B -> ps)))
3	2	r19.21adv 2181	. 2 |- (ph -> (x e. A -> A.y e. B ps))
4	3	r19.21aiv 2175	1 |- (ph -> A.x e. A A.y e. B ps)

Syntax hints:   -> wi 3   /\ wa 240   e. wcel 1300  A.wral 2105

This theorem is referenced by:  r19.21advv 2184  reuind 2450  wereu 3654  eufromeq5 3832  ralxp 4041  dom2d 5463  fiint 5650  ordiso 5683  ordtypelem5 5688  hartoglem 5692  rankxplim 5823  lbreu 7254  uzwo5OLD 7423  acdc3lem 8754  acdc2lem2 8758  acdc5lem2 8761  acdclem 8763  acdcALT 8765  tgcl 8894  topbas 8897  txbas 8933  blrn 9118  blf 9121  opntop 9147  tgbl 9148  blbas 9149  xpcn 9254  grpinvf 9364  grpdivf 9370  grplactf1o 9406  subgabl 9432  ghgrpi 9445  ssga 9455  nvmf 9598  va1cnlem 9684  ipf 9705  sspg 9726  ssps 9728  sspmlem 9730  0lno 9790  sspph 9856  ipblnfi 9857  filintf 10274  filfbas 10276  fsubbas 10281  fgfil 10290  extbas1 10291  filrn 10293  neifil 10302  usinuniop 10341  unmnd 10405  unopf1o 11477  cnvunop 11479  unoplin 11481  counop 11482  adjadj 11497  unopadj2 11499  hmopadj 11500  hmopadj2 11502  hmoplin 11503  bralnfn 11509  lnopmi 11562  lnopeq0i 11569  hmops 11582  hmopm 11583  hmopco 11585  lnopconi 11600  lnfnconi 11627  cnlnadjlem2 11638  adjlnop 11656  adjmul 11662  adjadd 11663  cdjreui 12004  bnj1367 13511  ghomf1olem 13637  dfon2 13858  nocvxmin 14029  axfelem10 14040  injrec 14461  injsurinj 14487  cbcpcp 14504  cbicplem 14508  toplat 14638  ltlga 14729  trooo 14758  muldisc 14824  inttop2 14863  hmeogrp 14892  homcard 14893  rcfpfillem4 14931  trnij 15015  dualded 15132  dualcat2 15133  idmon 15166  idfisf 15189  tarcrpr 15237  fictb 15371  ordisoOLD 15374  ordtypelem5OLD 15379  hartoglemOLD 15383  fitop 15401  iccconn 15453  2ndcctbss 15478  fness 15491  fnetr 15495  fnessref 15503  neibastop1 15518  topmtcl 15525  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  fnejoin2 15531  t1t0 15547  opnfbas 15557  isufil2 15565  filssufillem 15570  ufileulem 15572  ufileu 15573  filufint 15574  ufinffr 15578  ufilen 15579  filcon 15580  limfilcf 15587  flimcls 15588  rnelfmlem 15592  fmfnfmlem3 15596  fmfnfm 15598  fcluscf 15612  fclsfnflim 15614  flimfnfcls 15615  tailfb 15639  filnetlem3 15642  r19.21aivva 15653  eroprf 15735  pofun 15772  neificl 15841  metf1o 15843  metdcn 15853  ismtycnv 15949  ismtyhmeo 15951  ismtyres 15954  heiborlem15 15969  rrnmet 16016  isgrpda 16033  isablda 16035  pcoloopf 16079  pcohtpylem3 16082  isringd 16097  iscringd 16147  crnghomfo 16154  smprngpr 16200  ispridlc 16218  erprt 16276  prter2 16285  smoiso 16453  pointpsub 17231

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ral 2109

Copyright terms: Public domain