Theorem rspc2ev 3585

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

Step	Hyp	Ref	Expression
1		rspc2v.2	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
2	1	rspcev 3572	. . . 4 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒)
3	2	anim2i 617	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝐵 ∈ 𝐷 ∧ 𝜓)) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
4	3	3impb 1114	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
5		rspc2v.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
6	5	rexbidv 3156	. . 3 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝐷 𝜑 ↔ ∃𝑦 ∈ 𝐷 𝜒))
7	6	rspcev 3572	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)
8	4, 7	syl 17	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057

This theorem is referenced by:  2rspcedvdw  3586  rspc3ev  3589  opelxp  5655  fprb  7134  f1prex  7224  nf1const  7244  rspceov  7401  erov  8744  ralxpmap  8826  2dom  8958  elfiun  9320  dffi3  9321  ixpiunwdom  9482  1re  11118  hashdmpropge2  14396  wrdl2exs2  14859  ello12r  15430  ello1d  15436  elo12r  15441  o1lo1  15450  addcn2  15507  mulcn2  15509  bezoutlem3  16458  bezout  16460  pythagtriplem18  16750  pczpre  16765  pcdiv  16770  4sqlem3  16868  4sqlem4  16870  4sqlem12  16874  vdwlem1  16899  vdwlem6  16904  vdwlem8  16906  vdwlem12  16910  vdwlem13  16911  0ram  16938  ramz2  16942  cat1lem  18009  sgrp2rid2ex  18841  pmtr3ncom  19393  psgnunilem1  19411  irredn0  20347  isnzr2  20439  hausnei2  23274  cnhaus  23275  dishaus  23303  ordthauslem  23304  txuni2  23486  xkoopn  23510  txopn  23523  txdis  23553  txdis1cn  23556  pthaus  23559  txhaus  23568  tx1stc  23571  xkohaus  23574  regr1lem  23660  qustgplem  24042  methaus  24441  met2ndci  24443  metnrmlem3  24783  elplyr  26139  aaliou2b  26282  aaliou3lem9  26291  2irrexpq  26673  2irrexpqALT  26743  2sqlem2  27362  2sqlem8  27370  2sqlem11  27373  2sqb  27376  2sqnn0  27382  2sqnn  27383  pntibnd  27537  madecut  27834  mulsproplem12  28072  precsexlem11  28161  eucliddivs  28307  zzs12  28391  remulscllem1  28408  legov  28569  iscgrad  28795  f1otrge  28856  axsegconlem1  28902  axsegcon  28912  axpaschlem  28925  axlowdimlem6  28932  axlowdim1  28944  axlowdim2  28945  axeuclidlem  28947  umgrvad2edg  29198  wwlksnwwlksnon  29900  upgr4cycl4dv4e  30172  3cyclfrgrrn1  30272  4cycl2vnunb  30277  br8d  32598  lt2addrd  32741  xlt2addrd  32749  xrnarchi  33160  txomap  33854  tpr2rico  33932  qqhval2  34002  elsx  34214  br2base  34289  dya2iocnrect  34301  connpconn  35286  satfv1fvfmla1  35474  br8  35807  br4  35809  brsegle  36159  hilbert1.1  36205  nn0prpwlem  36373  knoppndvlem21  36583  poimirlem1  37667  itg2addnclem3  37719  cntotbnd  37842  smprngopr  38098  3dim2  39573  llni2  39617  lvoli3  39682  lvoli2  39686  islinei  39845  psubspi2N  39853  elpaddri  39907  eldioph2lem1  42858  diophin  42870  fphpdo  42915  irrapxlem3  42922  irrapxlem4  42923  pellexlem6  42932  pell1234qrreccl  42952  pell1234qrmulcl  42953  pell1234qrdich  42959  pell1qr1  42969  pellqrexplicit  42975  rmxycomplete  43015  dgraalem  43243  tfsconcatrev  43446  clsk3nimkb  44138  fourierdlem64  46273  rspceaov  47302  modn0mul  47462  ichnreuop  47577  prelspr  47591  reuopreuprim  47631  6gbe  47876  7gbow  47877  8gbe  47878  9gbo  47879  11gbo  47880  elbigo2r  48659  rrx2xpref1o  48824  inlinecirc02plem  48892  sepfsepc  49033  iscnrm3lem7  49044