Theorem rspc2ev 3573

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071

This theorem is referenced by:  rspc3ev  3575  opelxp  5626  fprb  7078  f1prex  7165  nf1const  7185  rspceov  7331  erov  8612  ralxpmap  8693  2dom  8829  elfiun  9198  dffi3  9199  ixpiunwdom  9358  1re  10984  hashdmpropge2  14206  wrdl2exs2  14668  ello12r  15235  ello1d  15241  elo12r  15246  o1lo1  15255  addcn2  15312  mulcn2  15314  bezoutlem3  16258  bezout  16260  pythagtriplem18  16542  pczpre  16557  pcdiv  16562  4sqlem3  16660  4sqlem4  16662  4sqlem12  16666  vdwlem1  16691  vdwlem6  16696  vdwlem8  16698  vdwlem12  16702  vdwlem13  16703  0ram  16730  ramz2  16734  cat1lem  17820  sgrp2rid2ex  18575  pmtr3ncom  19092  psgnunilem1  19110  irredn0  19954  isnzr2  20543  hausnei2  22513  cnhaus  22514  dishaus  22542  ordthauslem  22543  txuni2  22725  xkoopn  22749  txopn  22762  txdis  22792  txdis1cn  22795  pthaus  22798  txhaus  22807  tx1stc  22810  xkohaus  22813  regr1lem  22899  qustgplem  23281  methaus  23685  met2ndci  23687  metnrmlem3  24033  elplyr  25371  aaliou2b  25510  aaliou3lem9  25519  2irrexpq  25894  2irrexpqALT  25959  2sqlem2  26575  2sqlem8  26583  2sqlem11  26586  2sqb  26589  2sqnn0  26595  2sqnn  26596  pntibnd  26750  legov  26955  iscgrad  27181  f1otrge  27242  axsegconlem1  27294  axsegcon  27304  axpaschlem  27317  axlowdimlem6  27324  axlowdim1  27336  axlowdim2  27337  axeuclidlem  27339  umgrvad2edg  27589  wwlksnwwlksnon  28289  upgr4cycl4dv4e  28558  3cyclfrgrrn1  28658  4cycl2vnunb  28663  br8d  30959  lt2addrd  31083  xlt2addrd  31090  xrnarchi  31447  txomap  31793  tpr2rico  31871  qqhval2  31941  elsx  32171  isanmbfm  32232  br2base  32245  dya2iocnrect  32257  connpconn  33206  satfv1fvfmla1  33394  br8  33732  br4  33734  madecut  34074  brsegle  34419  hilbert1.1  34465  nn0prpwlem  34520  knoppndvlem21  34721  poimirlem1  35787  itg2addnclem3  35839  cntotbnd  35963  smprngopr  36219  3dim2  37489  llni2  37533  lvoli3  37598  lvoli2  37602  islinei  37761  psubspi2N  37769  elpaddri  37823  2rspcedvdw  40187  eldioph2lem1  40589  diophin  40601  fphpdo  40646  irrapxlem3  40653  irrapxlem4  40654  pellexlem6  40663  pell1234qrreccl  40683  pell1234qrmulcl  40684  pell1234qrdich  40690  pell1qr1  40700  pellqrexplicit  40706  rmxycomplete  40746  dgraalem  40977  clsk3nimkb  41657  fourierdlem64  43718  rspceaov  44700  ichnreuop  44935  prelspr  44949  reuopreuprim  44989  6gbe  45234  7gbow  45235  8gbe  45236  9gbo  45237  11gbo  45238  modn0mul  45877  elbigo2r  45910  rrx2xpref1o  46075  inlinecirc02plem  46143  sepfsepc  46232  iscnrm3lem7  46244