Theorem rspc2ev 3575

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

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

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 2707

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 2714  df-cleq 2727  df-clel 2810  df-ral 3050  df-rex 3060

This theorem is referenced by:  2rspcedvdw  3576  opelxp  5656  fprb  7138  f1prex  7228  nf1const  7248  rspceov  7405  erov  8750  ralxpmap  8833  2dom  8966  elfiun  9332  dffi3  9333  ixpiunwdom  9494  1re  11133  hashdmpropge2  14434  wrdl2exs2  14897  ello12r  15468  ello1d  15474  elo12r  15479  o1lo1  15488  addcn2  15545  mulcn2  15547  bezoutlem3  16499  bezout  16501  pythagtriplem18  16792  pczpre  16807  pcdiv  16812  4sqlem3  16910  4sqlem4  16912  4sqlem12  16916  vdwlem1  16941  vdwlem6  16946  vdwlem8  16948  vdwlem12  16952  vdwlem13  16953  0ram  16980  ramz2  16984  cat1lem  18052  sgrp2rid2ex  18887  pmtr3ncom  19439  psgnunilem1  19457  irredn0  20392  isnzr2  20484  hausnei2  23306  cnhaus  23307  dishaus  23335  ordthauslem  23336  txuni2  23518  xkoopn  23542  txopn  23555  txdis  23585  txdis1cn  23588  pthaus  23591  txhaus  23600  tx1stc  23603  xkohaus  23606  regr1lem  23692  qustgplem  24074  methaus  24473  met2ndci  24475  metnrmlem3  24815  elplyr  26154  aaliou2b  26295  aaliou3lem9  26304  2irrexpq  26683  2irrexpqALT  26752  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  29971  upgr4cycl4dv4e  30243  3cyclfrgrrn1  30343  4cycl2vnunb  30348  br8d  32669  lt2addrd  32811  xlt2addrd  32820  xrnarchi  33233  txomap  33966  tpr2rico  34044  qqhval2  34114  elsx  34326  br2base  34401  dya2iocnrect  34413  connpconn  35405  satfv1fvfmla1  35593  br8  35926  br4  35928  brsegle  36278  hilbert1.1  36324  nn0prpwlem  36492  knoppndvlem21  36780  poimirlem1  37930  itg2addnclem3  37982  cntotbnd  38105  smprngopr  38361  3dim2  39902  llni2  39946  lvoli3  40011  lvoli2  40015  islinei  40174  psubspi2N  40182  elpaddri  40236  eldioph2lem1  43180  diophin  43192  fphpdo  43233  irrapxlem3  43240  irrapxlem4  43241  pellexlem6  43250  pell1234qrreccl  43270  pell1234qrmulcl  43271  pell1234qrdich  43277  pell1qr1  43287  pellqrexplicit  43293  rmxycomplete  43333  dgraalem  43561  tfsconcatrev  43764  clsk3nimkb  44455  fourierdlem64  46586  rspceaov  47633  modn0mul  47799  ichnreuop  47920  prelspr  47934  reuopreuprim  47974  6gbe  48235  7gbow  48236  8gbe  48237  9gbo  48238  11gbo  48239  elbigo2r  49017  rrx2xpref1o  49182  inlinecirc02plem  49250  sepfsepc  49391  iscnrm3lem7  49402