Theorem rspc2ev 3578

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063

This theorem is referenced by:  2rspcedvdw  3579  rspc3ev  3582  opelxp  5658  fprb  7140  f1prex  7230  nf1const  7250  rspceov  7407  erov  8752  ralxpmap  8835  2dom  8968  elfiun  9334  dffi3  9335  ixpiunwdom  9496  1re  11133  hashdmpropge2  14407  wrdl2exs2  14870  ello12r  15441  ello1d  15447  elo12r  15452  o1lo1  15461  addcn2  15518  mulcn2  15520  bezoutlem3  16469  bezout  16471  pythagtriplem18  16761  pczpre  16776  pcdiv  16781  4sqlem3  16879  4sqlem4  16881  4sqlem12  16885  vdwlem1  16910  vdwlem6  16915  vdwlem8  16917  vdwlem12  16921  vdwlem13  16922  0ram  16949  ramz2  16953  cat1lem  18021  sgrp2rid2ex  18856  pmtr3ncom  19408  psgnunilem1  19426  irredn0  20361  isnzr2  20453  hausnei2  23296  cnhaus  23297  dishaus  23325  ordthauslem  23326  txuni2  23508  xkoopn  23532  txopn  23545  txdis  23575  txdis1cn  23578  pthaus  23581  txhaus  23590  tx1stc  23593  xkohaus  23596  regr1lem  23682  qustgplem  24064  methaus  24463  met2ndci  24465  metnrmlem3  24805  elplyr  26147  aaliou2b  26289  aaliou3lem9  26298  2irrexpq  26680  2irrexpqALT  26750  2sqlem2  27369  2sqlem8  27377  2sqlem11  27380  2sqb  27383  2sqnn0  27389  2sqnn  27390  pntibnd  27544  madecut  27863  mulsproplem12  28107  precsexlem11  28197  eucliddivs  28356  elz12si  28453  zz12s  28455  remulscllem1  28480  legov  28641  iscgrad  28867  f1otrge  28928  axsegconlem1  28974  axsegcon  28984  axpaschlem  28997  axlowdimlem6  29004  axlowdim1  29016  axlowdim2  29017  axeuclidlem  29019  umgrvad2edg  29270  wwlksnwwlksnon  29972  upgr4cycl4dv4e  30244  3cyclfrgrrn1  30344  4cycl2vnunb  30349  br8d  32670  lt2addrd  32813  xlt2addrd  32822  xrnarchi  33250  txomap  33984  tpr2rico  34062  qqhval2  34132  elsx  34344  br2base  34419  dya2iocnrect  34431  connpconn  35423  satfv1fvfmla1  35611  br8  35944  br4  35946  brsegle  36296  hilbert1.1  36342  nn0prpwlem  36510  knoppndvlem21  36790  poimirlem1  37933  itg2addnclem3  37985  cntotbnd  38108  smprngopr  38364  3dim2  39905  llni2  39949  lvoli3  40014  lvoli2  40018  islinei  40177  psubspi2N  40185  elpaddri  40239  eldioph2lem1  43191  diophin  43203  fphpdo  43248  irrapxlem3  43255  irrapxlem4  43256  pellexlem6  43265  pell1234qrreccl  43285  pell1234qrmulcl  43286  pell1234qrdich  43292  pell1qr1  43302  pellqrexplicit  43308  rmxycomplete  43348  dgraalem  43576  tfsconcatrev  43779  clsk3nimkb  44470  fourierdlem64  46602  rspceaov  47631  modn0mul  47791  ichnreuop  47906  prelspr  47920  reuopreuprim  47960  6gbe  48205  7gbow  48206  8gbe  48207  9gbo  48208  11gbo  48209  elbigo2r  48987  rrx2xpref1o  49152  inlinecirc02plem  49220  sepfsepc  49361  iscnrm3lem7  49372