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

Theorem rspc2ev 3621
Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)
Hypotheses
Ref Expression
rspc2v.1 (𝑥 = 𝐴 → (𝜑𝜒))
rspc2v.2 (𝑦 = 𝐵 → (𝜒𝜓))
Assertion
Ref Expression
rspc2ev ((𝐴𝐶𝐵𝐷𝜓) → ∃𝑥𝐶𝑦𝐷 𝜑)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝐷,𝑦   𝜒,𝑥   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑦)   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem rspc2ev
StepHypRef Expression
1 rspc2v.2 . . . . 5 (𝑦 = 𝐵 → (𝜒𝜓))
21rspcev 3608 . . . 4 ((𝐵𝐷𝜓) → ∃𝑦𝐷 𝜒)
32anim2i 615 . . 3 ((𝐴𝐶 ∧ (𝐵𝐷𝜓)) → (𝐴𝐶 ∧ ∃𝑦𝐷 𝜒))
433impb 1112 . 2 ((𝐴𝐶𝐵𝐷𝜓) → (𝐴𝐶 ∧ ∃𝑦𝐷 𝜒))
5 rspc2v.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜒))
65rexbidv 3169 . . 3 (𝑥 = 𝐴 → (∃𝑦𝐷 𝜑 ↔ ∃𝑦𝐷 𝜒))
76rspcev 3608 . 2 ((𝐴𝐶 ∧ ∃𝑦𝐷 𝜒) → ∃𝑥𝐶𝑦𝐷 𝜑)
84, 7syl 17 1 ((𝐴𝐶𝐵𝐷𝜓) → ∃𝑥𝐶𝑦𝐷 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wrex 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061
This theorem is referenced by:  2rspcedvdw  3622  rspc3ev  3625  opelxp  5720  fprb  7213  f1prex  7300  nf1const  7319  rspceov  7474  erov  8845  ralxpmap  8927  2dom  9068  elfiun  9475  dffi3  9476  ixpiunwdom  9635  1re  11266  hashdmpropge2  14504  wrdl2exs2  14957  ello12r  15521  ello1d  15527  elo12r  15532  o1lo1  15541  addcn2  15598  mulcn2  15600  bezoutlem3  16544  bezout  16546  pythagtriplem18  16836  pczpre  16851  pcdiv  16856  4sqlem3  16954  4sqlem4  16956  4sqlem12  16960  vdwlem1  16985  vdwlem6  16990  vdwlem8  16992  vdwlem12  16996  vdwlem13  16997  0ram  17024  ramz2  17028  cat1lem  18120  sgrp2rid2ex  18919  pmtr3ncom  19475  psgnunilem1  19493  irredn0  20407  isnzr2  20502  hausnei2  23351  cnhaus  23352  dishaus  23380  ordthauslem  23381  txuni2  23563  xkoopn  23587  txopn  23600  txdis  23630  txdis1cn  23633  pthaus  23636  txhaus  23645  tx1stc  23648  xkohaus  23651  regr1lem  23737  qustgplem  24119  methaus  24523  met2ndci  24525  metnrmlem3  24871  elplyr  26231  aaliou2b  26372  aaliou3lem9  26381  2irrexpq  26761  2irrexpqALT  26831  2sqlem2  27450  2sqlem8  27458  2sqlem11  27461  2sqb  27464  2sqnn0  27470  2sqnn  27471  pntibnd  27625  madecut  27909  mulsproplem12  28131  precsexlem11  28219  remulscllem1  28354  legov  28515  iscgrad  28741  f1otrge  28802  axsegconlem1  28854  axsegcon  28864  axpaschlem  28877  axlowdimlem6  28884  axlowdim1  28896  axlowdim2  28897  axeuclidlem  28899  umgrvad2edg  29152  wwlksnwwlksnon  29852  upgr4cycl4dv4e  30121  3cyclfrgrrn1  30221  4cycl2vnunb  30226  br8d  32532  lt2addrd  32657  xlt2addrd  32664  xrnarchi  33051  txomap  33651  tpr2rico  33729  qqhval2  33799  elsx  34029  br2base  34105  dya2iocnrect  34117  connpconn  35065  satfv1fvfmla1  35253  br8  35580  br4  35582  brsegle  35934  hilbert1.1  35980  nn0prpwlem  36036  knoppndvlem21  36237  poimirlem1  37324  itg2addnclem3  37376  cntotbnd  37499  smprngopr  37755  3dim2  39169  llni2  39213  lvoli3  39278  lvoli2  39282  islinei  39441  psubspi2N  39449  elpaddri  39503  eldioph2lem1  42435  diophin  42447  fphpdo  42492  irrapxlem3  42499  irrapxlem4  42500  pellexlem6  42509  pell1234qrreccl  42529  pell1234qrmulcl  42530  pell1234qrdich  42536  pell1qr1  42546  pellqrexplicit  42552  rmxycomplete  42593  dgraalem  42824  tfsconcatrev  43032  clsk3nimkb  43725  fourierdlem64  45809  rspceaov  46828  ichnreuop  47062  prelspr  47076  reuopreuprim  47116  6gbe  47361  7gbow  47362  8gbe  47363  9gbo  47364  11gbo  47365  modn0mul  47926  elbigo2r  47959  rrx2xpref1o  48124  inlinecirc02plem  48192  sepfsepc  48279  iscnrm3lem7  48291
  Copyright terms: Public domain W3C validator