Theorem rspc2ev 3593

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1102   = wceq 1569   ∈ wcel 2142  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089

This theorem is used by:  2rspcedvdw  3594  opelxp  5696  fprb  7192  f1prex  7282  nf1const  7302  rspceov  7461  erov  8810  ralxpmap  8892  2dom  9025  elfiun  9388  dffi3  9389  ixpiunwdom  9550  1re  11214  hashdmpropge2  14527  wrdl2exs2  14990  ello12r  15575  ello1d  15581  elo12r  15586  o1lo1  15595  addcn2  15652  mulcn2  15654  bezoutlem3  16605  bezout  16607  pythagtriplem18  16898  pczpre  16913  pcdiv  16918  4sqlem3  17016  4sqlem4  17018  4sqlem12  17022  vdwlem1  17047  vdwlem6  17052  vdwlem8  17054  vdwlem12  17058  vdwlem13  17059  0ram  17086  ramz2  17090  cat1lem  18159  sgrp2rid2ex  18995  pmtr3ncom  19551  psgnunilem1  19569  irredn0  20512  isnzr2  20626  hausnei2  23521  cnhaus  23522  dishaus  23550  ordthauslem  23551  txuni2  23733  xkoopn  23757  txopn  23770  txdis  23800  txdis1cn  23803  pthaus  23806  txhaus  23815  tx1stc  23818  xkohaus  23821  regr1lem  23907  qustgplem  24289  methaus  24688  met2ndci  24690  metnrmlem3  25030  elplyr  26369  aaliou2b  26515  aaliou3lem9  26524  2irrexpq  26907  2irrexpqALT  26976  2sqlem2  27593  2sqlem8  27601  2sqlem11  27604  2sqb  27607  2sqnn  27614  pntibnd  27768  madecut  28087  mulsproplem12  28331  precsexlem11  28421  eucliddivs  28580  elz12si  28677  zz12s  28679  remulscllem1  28704  legov  28865  iscgrad  29133  f1otrge  29232  axsegconlem1  29278  axsegcon  29288  axpaschlem  29301  axlowdimlem6  29308  axlowdim1  29320  axlowdim2  29321  axeuclidlem  29323  umgrvad2edg  29574  wwlksnwwlksnon  30275  upgr4cycl4dv4e  30547  3cyclfrgrrn1  30647  4cycl2vnunb  30652  br8d  32964  lt2addrd  33106  xlt2addrd  33115  xrnarchi  33513  txomap  34233  tpr2rico  34311  qqhval2  34381  elsx  34593  br2base  34668  dya2iocnrect  34680  connpconn  35735  satfv1fvfmla1  35923  br8  36256  br4  36258  brsegle  36608  hilbert1.1  36654  nn0prpwlem  36861  knoppndvlem21  37149  poimirlem1  38300  itg2addnclem3  38352  cntotbnd  38475  smprngopr  38731  3dim2  40270  llni2  40314  lvoli3  40379  lvoli2  40383  islinei  40542  psubspi2N  40550  elpaddri  40604  eldioph2lem1  43519  diophin  43531  fphpdo  43572  irrapxlem3  43579  irrapxlem4  43580  pellexlem6  43589  pell1234qrreccl  43609  pell1234qrmulcl  43610  pell1234qrdich  43616  pell1qr1  43626  pellqrexplicit  43632  rmxycomplete  43672  dgraalem  43900  tfsconcatrev  44103  clsk3nimkb  44794  fourierdlem64  46912  rspceaov  47962  modn0mul  48128  ichnreuop  48249  prelspr  48263  reuopreuprim  48303  6gbe  48564  7gbow  48565  8gbe  48566  9gbo  48567  11gbo  48568  smprngprmrng  49132  elbigo2r  49361  rrx2xpref1o  49526  inlinecirc02plem  49594  sepfsepc  49734  iscnrm3lem7  49745