Theorem rspc2ev 3592

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089

This theorem is used by:  2rspcedvdw  3593  opelxp  5695  fprb  7195  f1prex  7288  nf1const  7308  rspceov  7465  erov  8817  ralxpmap  8906  2dom  9040  elfiun  9403  dffi3  9404  ixpiunwdom  9565  1re  11235  hashdmpropge2  14550  wrdl2exs2  15019  ello12r  15606  ello1d  15612  elo12r  15617  o1lo1  15626  addcn2  15683  mulcn2  15685  bezoutlem3  16635  bezout  16637  pythagtriplem18  16928  pczpre  16943  pcdiv  16948  4sqlem3  17046  4sqlem4  17048  4sqlem12  17052  vdwlem1  17077  vdwlem6  17082  vdwlem8  17084  vdwlem12  17088  vdwlem13  17089  0ram  17116  ramz2  17120  cat1lem  18189  sgrp2rid2ex  19040  pmtr3ncom  19603  psgnunilem1  19621  irredn0  20565  isnzr2  20679  hausnei2  23579  cnhaus  23580  dishaus  23608  ordthauslem  23609  txuni2  23792  xkoopn  23816  txopn  23829  txdis  23859  txdis1cn  23862  pthaus  23865  txhaus  23874  tx1stc  23877  xkohaus  23880  regr1lem  23966  qustgplem  24348  methaus  24747  met2ndci  24749  metnrmlem3  25089  elplyr  26428  aaliou2b  26574  aaliou3lem9  26583  2irrexpq  26966  2irrexpqALT  27035  2sqlem2  27652  2sqlem8  27660  2sqlem11  27663  2sqb  27666  2sqnn  27673  pntibnd  27827  madecut  28146  mulsproplem12  28390  precsexlem11  28480  eucliddivs  28639  elz12si  28736  zz12s  28738  remulscllem1  28763  legov  28925  iscgrad  29195  f1otrge  29314  axsegconlem1  29360  axsegcon  29370  axpaschlem  29383  axlowdimlem6  29390  axlowdim1  29402  axlowdim2  29403  axeuclidlem  29405  umgrvad2edg  29659  wwlksnwwlksnon  30369  upgr4cycl4dv4e  30651  3cyclfrgrrn1  30751  4cycl2vnunb  30756  br8d  33068  lt2addrd  33208  xlt2addrd  33217  xrnarchi  33611  txomap  34331  tpr2rico  34409  qqhval2  34479  elsx  34692  br2base  34767  dya2iocnrect  34779  connpconn  35801  satfv1fvfmla1  35989  br8  36322  br4  36324  brsegle  36675  hilbert1.1  36721  nn0prpwlem  36928  knoppndvlem21  37216  poimirlem1  38357  itg2addnclem3  38409  cntotbnd  38533  smprngopr  38789  3dim2  40328  llni2  40372  lvoli3  40437  lvoli2  40441  islinei  40600  psubspi2N  40608  elpaddri  40662  eldioph2lem1  43592  diophin  43604  fphpdo  43645  irrapxlem3  43652  irrapxlem4  43653  pellexlem6  43662  pell1234qrreccl  43682  pell1234qrmulcl  43683  pell1234qrdich  43689  pell1qr1  43699  pellqrexplicit  43705  rmxycomplete  43745  dgraalem  43973  tfsconcatrev  44176  clsk3nimkb  44867  fourierdlem64  46985  rspceaov  48072  modn0mul  48238  ichnreuop  48359  prelspr  48373  reuopreuprim  48413  6gbe  48674  7gbow  48675  8gbe  48676  9gbo  48677  11gbo  48678  smprngprmrng  49241  elbigo2r  49470  rrx2xpref1o  49635  inlinecirc02plem  49703  sepfsepc  49841  iscnrm3lem7  49852