Theorem rspc2ev 3355

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  ∃wrex 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-v 3233

This theorem is referenced by:  rspc3ev  3357  opelxp  5180  f1prex  6579  rspceov  6732  erov  7887  ralxpmap  7949  2dom  8070  elfiun  8377  dffi3  8378  ixpiunwdom  8537  1re  10077  hashdmpropge2  13303  wrdl2exs2  13736  ello12r  14292  ello1d  14298  elo12r  14303  o1lo1  14312  addcn2  14368  mulcn2  14370  bezoutlem3  15305  bezout  15307  pythagtriplem18  15584  pczpre  15599  pcdiv  15604  4sqlem3  15701  4sqlem4  15703  4sqlem12  15707  vdwlem1  15732  vdwlem6  15737  vdwlem8  15739  vdwlem12  15743  vdwlem13  15744  0ram  15771  ramz2  15775  sgrp2rid2ex  17461  pmtr3ncom  17941  psgnunilem1  17959  irredn0  18749  isnzr2  19311  hausnei2  21205  cnhaus  21206  dishaus  21234  ordthauslem  21235  txuni2  21416  xkoopn  21440  txopn  21453  txdis  21483  txdis1cn  21486  pthaus  21489  txhaus  21498  tx1stc  21501  xkohaus  21504  regr1lem  21590  qustgplem  21971  methaus  22372  met2ndci  22374  metnrmlem3  22711  elplyr  24002  aaliou2b  24141  aaliou3lem9  24150  2sqlem2  25188  2sqlem8  25196  2sqlem11  25199  2sqb  25202  pntibnd  25327  legov  25525  iscgrad  25748  f1otrge  25797  axsegconlem1  25842  axsegcon  25852  axpaschlem  25865  axlowdimlem6  25872  axlowdim1  25884  axlowdim2  25885  axeuclidlem  25887  structgrssvtxlemOLD  25960  umgrvad2edg  26150  wwlksnwwlksnon  26878  wwlksnwwlksnonOLD  26880  upgr4cycl4dv4e  27163  3cyclfrgrrn1  27265  4cycl2vnunb  27270  br8d  29548  lt2addrd  29644  xlt2addrd  29651  xrnarchi  29866  txomap  30029  tpr2rico  30086  qqhval2  30154  elsx  30385  isanmbfm  30446  br2base  30459  dya2iocnrect  30471  connpconn  31343  br8  31772  br4  31774  fprb  31795  brsegle  32340  hilbert1.1  32386  nn0prpwlem  32442  knoppndvlem21  32648  poimirlem1  33540  itg2addnclem3  33593  cntotbnd  33725  smprngopr  33981  3dim2  35072  llni2  35116  lvoli3  35181  lvoli2  35185  islinei  35344  psubspi2N  35352  elpaddri  35406  eldioph2lem1  37640  diophin  37653  fphpdo  37698  irrapxlem3  37705  irrapxlem4  37706  pellexlem6  37715  pell1234qrreccl  37735  pell1234qrmulcl  37736  pell1234qrdich  37742  pell1qr1  37752  pellqrexplicit  37758  rmxycomplete  37799  dgraalem  38032  clsk3nimkb  38655  fourierdlem64  40705  rspceaov  41598  6gbe  41984  7gbow  41985  8gbe  41986  9gbo  41987  11gbo  41988  prelspr  42061  modn0mul  42640  elbigo2r  42672