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

Theorem rspc2ev 3291
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 3278 . . . 4 ((𝐵𝐷𝜓) → ∃𝑦𝐷 𝜒)
32anim2i 590 . . 3 ((𝐴𝐶 ∧ (𝐵𝐷𝜓)) → (𝐴𝐶 ∧ ∃𝑦𝐷 𝜒))
433impb 1251 . 2 ((𝐴𝐶𝐵𝐷𝜓) → (𝐴𝐶 ∧ ∃𝑦𝐷 𝜒))
5 rspc2v.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜒))
65rexbidv 3030 . . 3 (𝑥 = 𝐴 → (∃𝑦𝐷 𝜑 ↔ ∃𝑦𝐷 𝜒))
76rspcev 3278 . 2 ((𝐴𝐶 ∧ ∃𝑦𝐷 𝜒) → ∃𝑥𝐶𝑦𝐷 𝜑)
84, 7syl 17 1 ((𝐴𝐶𝐵𝐷𝜓) → ∃𝑥𝐶𝑦𝐷 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wrex 2893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rex 2898  df-v 3171
This theorem is referenced by:  rspc3ev  3293  opelxp  5057  f1prex  6414  rspceov  6565  erov  7705  ralxpmap  7767  2dom  7889  elfiun  8193  dffi3  8194  ixpiunwdom  8353  1re  9892  wrdl2exs2  13481  ello12r  14039  ello1d  14045  elo12r  14050  o1lo1  14059  addcn2  14115  mulcn2  14117  bezoutlem3  15039  bezout  15041  pythagtriplem18  15318  pczpre  15333  pcdiv  15338  4sqlem3  15435  4sqlem4  15437  4sqlem12  15441  vdwlem1  15466  vdwlem6  15471  vdwlem8  15473  vdwlem12  15477  vdwlem13  15478  0ram  15505  ramz2  15509  sgrp2rid2ex  17180  pmtr3ncom  17661  psgnunilem1  17679  irredn0  18469  isnzr2  19027  hausnei2  20906  cnhaus  20907  dishaus  20935  ordthauslem  20936  txuni2  21117  xkoopn  21141  txopn  21154  txdis  21184  txdis1cn  21187  pthaus  21190  txhaus  21199  tx1stc  21202  xkohaus  21205  regr1lem  21291  qustgplem  21673  methaus  22073  met2ndci  22075  metnrmlem3  22400  elplyr  23675  aaliou2b  23814  aaliou3lem9  23823  2sqlem2  24857  2sqlem8  24865  2sqlem11  24868  2sqb  24871  pntibnd  24996  legov  25195  iscgrad  25418  f1otrge  25467  axsegconlem1  25512  axsegcon  25522  axpaschlem  25535  axlowdimlem6  25542  axlowdim1  25554  axlowdim2  25555  axeuclidlem  25557  el2wlksotot  26172  3cyclfrgrarn1  26302  4cycl2vnunb  26307  br8d  28605  lt2addrd  28706  xlt2addrd  28716  xrnarchi  28872  txomap  29032  tpr2rico  29089  qqhval2  29157  elsx  29387  isanmbfm  29448  br2base  29461  dya2iocnrect  29473  conpcon  30274  br8  30702  br4  30704  fprb  30719  brsegle  31188  hilbert1.1  31234  nn0prpwlem  31290  knoppndvlem21  31496  poimirlem1  32380  itg2addnclem3  32433  cntotbnd  32565  smprngopr  32821  3dim2  33572  llni2  33616  lvoli3  33681  lvoli2  33685  islinei  33844  psubspi2N  33852  elpaddri  33906  eldioph2lem1  36141  diophin  36154  fphpdo  36199  irrapxlem3  36206  irrapxlem4  36207  pellexlem6  36216  pell1234qrreccl  36236  pell1234qrmulcl  36237  pell1234qrdich  36243  pell1qr1  36253  pellqrexplicit  36259  rmxycomplete  36300  dgraalem  36534  clsk3nimkb  37158  fourierdlem64  38864  rspceaov  39728  6gbe  39995  7gbo  39996  8gbe  39997  9gboa  39998  11gboa  39999  structgrssvtxlem  40255  upgredg  40369  umgrvad2edg  40439  wwlksnwwlksnon  41120  upgr4cycl4dv4e  41351  3cyclfrgrrn1  41454  4cycl2vnunb-av  41459  modn0mul  42108  elbigo2r  42144
  Copyright terms: Public domain W3C validator