Theorem rspc2ev 3632

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1082   = wceq 1536   ∈ wcel 2113  ∃wrex 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1084  df-ex 1780  df-cleq 2813  df-clel 2892  df-ral 3142  df-rex 3143

This theorem is referenced by:  rspc3ev  3634  opelxp  5584  fprb  6949  f1prex  7033  nf1const  7052  rspceov  7196  erov  8387  ralxpmap  8453  2dom  8575  elfiun  8887  dffi3  8888  ixpiunwdom  9048  1re  10634  hashdmpropge2  13838  wrdl2exs2  14303  ello12r  14869  ello1d  14875  elo12r  14880  o1lo1  14889  addcn2  14945  mulcn2  14947  bezoutlem3  15884  bezout  15886  pythagtriplem18  16164  pczpre  16179  pcdiv  16184  4sqlem3  16281  4sqlem4  16283  4sqlem12  16287  vdwlem1  16312  vdwlem6  16317  vdwlem8  16319  vdwlem12  16323  vdwlem13  16324  0ram  16351  ramz2  16355  sgrp2rid2ex  18087  pmtr3ncom  18598  psgnunilem1  18616  irredn0  19448  isnzr2  20031  hausnei2  21956  cnhaus  21957  dishaus  21985  ordthauslem  21986  txuni2  22168  xkoopn  22192  txopn  22205  txdis  22235  txdis1cn  22238  pthaus  22241  txhaus  22250  tx1stc  22253  xkohaus  22256  regr1lem  22342  qustgplem  22724  methaus  23125  met2ndci  23127  metnrmlem3  23464  elplyr  24789  aaliou2b  24928  aaliou3lem9  24937  2irrexpq  25311  2irrexpqALT  25376  2sqlem2  25992  2sqlem8  26000  2sqlem11  26003  2sqb  26006  2sqnn0  26012  2sqnn  26013  pntibnd  26167  legov  26369  iscgrad  26595  f1otrge  26656  axsegconlem1  26701  axsegcon  26711  axpaschlem  26724  axlowdimlem6  26731  axlowdim1  26743  axlowdim2  26744  axeuclidlem  26746  umgrvad2edg  26993  wwlksnwwlksnon  27692  upgr4cycl4dv4e  27962  3cyclfrgrrn1  28062  4cycl2vnunb  28067  br8d  30361  lt2addrd  30475  xlt2addrd  30482  xrnarchi  30834  txomap  31122  tpr2rico  31176  qqhval2  31244  elsx  31474  isanmbfm  31535  br2base  31548  dya2iocnrect  31560  connpconn  32503  satfv1fvfmla1  32691  br8  33013  br4  33015  brsegle  33590  hilbert1.1  33636  nn0prpwlem  33691  knoppndvlem21  33892  poimirlem1  34928  itg2addnclem3  34980  cntotbnd  35107  smprngopr  35363  3dim2  36637  llni2  36681  lvoli3  36746  lvoli2  36750  islinei  36909  psubspi2N  36917  elpaddri  36971  eldioph2lem1  39433  diophin  39445  fphpdo  39490  irrapxlem3  39497  irrapxlem4  39498  pellexlem6  39507  pell1234qrreccl  39527  pell1234qrmulcl  39528  pell1234qrdich  39534  pell1qr1  39544  pellqrexplicit  39550  rmxycomplete  39590  dgraalem  39821  clsk3nimkb  40464  fourierdlem64  42529  rspceaov  43470  ichnreuop  43708  prelspr  43722  reuopreuprim  43762  6gbe  44010  7gbow  44011  8gbe  44012  9gbo  44013  11gbo  44014  modn0mul  44654  elbigo2r  44687  rrx2xpref1o  44779  inlinecirc02plem  44847