Theorem rspc2ev 3595

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 3582	. . . 4 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒)
3	2	anim2i 626	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝐵 ∈ 𝐷 ∧ 𝜓)) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
4	3	3impb 1128	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
5		rspc2v.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
6	5	rexbidv 3187	. . 3 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝐷 𝜑 ↔ ∃𝑦 ∈ 𝐷 𝜒))
7	6	rspcev 3582	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)
8	4, 7	syl 17	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1099   = wceq 1561   ∈ wcel 2143  ∃wrex 3087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3078  df-rex 3088

This theorem is referenced by:  2rspcedvdw  3596  opelxp  5684  fprb  7178  f1prex  7268  nf1const  7288  rspceov  7445  erov  8796  ralxpmap  8878  2dom  9011  elfiun  9374  dffi3  9375  ixpiunwdom  9536  1re  11192  hashdmpropge2  14506  wrdl2exs2  14969  ello12r  15554  ello1d  15560  elo12r  15565  o1lo1  15574  addcn2  15631  mulcn2  15633  bezoutlem3  16585  bezout  16587  pythagtriplem18  16878  pczpre  16893  pcdiv  16898  4sqlem3  16996  4sqlem4  16998  4sqlem12  17002  vdwlem1  17027  vdwlem6  17032  vdwlem8  17034  vdwlem12  17038  vdwlem13  17039  0ram  17066  ramz2  17070  cat1lem  18139  sgrp2rid2ex  18974  pmtr3ncom  19525  psgnunilem1  19543  irredn0  20482  isnzr2  20578  hausnei2  23420  cnhaus  23421  dishaus  23449  ordthauslem  23450  txuni2  23632  xkoopn  23656  txopn  23669  txdis  23699  txdis1cn  23702  pthaus  23705  txhaus  23714  tx1stc  23717  xkohaus  23720  regr1lem  23806  qustgplem  24188  methaus  24587  met2ndci  24589  metnrmlem3  24929  elplyr  26268  aaliou2b  26412  aaliou3lem9  26421  2irrexpq  26803  2irrexpqALT  26872  2sqlem2  27489  2sqlem8  27497  2sqlem11  27500  2sqb  27503  2sqnn0  27509  2sqnn  27510  pntibnd  27664  madecut  27983  mulsproplem12  28227  precsexlem11  28317  eucliddivs  28476  elz12si  28573  zz12s  28575  remulscllem1  28600  legov  28761  iscgrad  29012  f1otrge  29079  axsegconlem1  29125  axsegcon  29135  axpaschlem  29148  axlowdimlem6  29155  axlowdim1  29167  axlowdim2  29168  axeuclidlem  29170  umgrvad2edg  29421  wwlksnwwlksnon  30122  upgr4cycl4dv4e  30394  3cyclfrgrrn1  30494  4cycl2vnunb  30499  br8d  32816  lt2addrd  32958  xlt2addrd  32967  xrnarchi  33370  txomap  34133  tpr2rico  34211  qqhval2  34281  elsx  34493  br2base  34568  dya2iocnrect  34580  connpconn  35590  satfv1fvfmla1  35778  br8  36111  br4  36113  brsegle  36463  hilbert1.1  36509  nn0prpwlem  36687  knoppndvlem21  36975  poimirlem1  38125  itg2addnclem3  38177  cntotbnd  38300  smprngopr  38556  3dim2  40097  llni2  40141  lvoli3  40206  lvoli2  40210  islinei  40369  psubspi2N  40377  elpaddri  40431  eldioph2lem1  43346  diophin  43358  fphpdo  43399  irrapxlem3  43406  irrapxlem4  43407  pellexlem6  43416  pell1234qrreccl  43436  pell1234qrmulcl  43437  pell1234qrdich  43443  pell1qr1  43453  pellqrexplicit  43459  rmxycomplete  43499  dgraalem  43727  tfsconcatrev  43930  clsk3nimkb  44621  fourierdlem64  46735  rspceaov  47782  modn0mul  47948  ichnreuop  48069  prelspr  48083  reuopreuprim  48123  6gbe  48384  7gbow  48385  8gbe  48386  9gbo  48387  11gbo  48388  elbigo2r  49166  rrx2xpref1o  49331  inlinecirc02plem  49399  sepfsepc  49540  iscnrm3lem7  49551