Theorem rspc2ev 3324

Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)

Hypotheses

Ref	Expression
rspc2v.1	|- ( x = A -> ( ph <-> ch ) )
rspc2v.2	|- ( y = B -> ( ch <-> ps ) )

Assertion

Ref	Expression
rspc2ev	|- ( ( A e. C /\ B e. D /\ ps ) -> E. x e. C E. y e. D ph )

Distinct variable groups:   x, y, A   y, B   x, C   x, D, y   ch, x   ps, y

Allowed substitution hints:   ph( x, y)   ps( x)   ch( y)   B( x)   C( y)

Proof of Theorem rspc2ev

Step	Hyp	Ref	Expression
1		rspc2v.2	. . . . 5 |- ( y = B -> ( ch <-> ps ) )
2	1	rspcev 3309	. . . 4 |- ( ( B e. D /\ ps ) -> E. y e. D ch )
3	2	anim2i 593	. . 3 |- ( ( A e. C /\ ( B e. D /\ ps ) ) -> ( A e. C /\ E. y e. D ch ) )
4	3	3impb 1260	. 2 |- ( ( A e. C /\ B e. D /\ ps ) -> ( A e. C /\ E. y e. D ch ) )
5		rspc2v.1	. . . 4 |- ( x = A -> ( ph <-> ch ) )
6	5	rexbidv 3052	. . 3 |- ( x = A -> ( E. y e. D ph <-> E. y e. D ch ) )
7	6	rspcev 3309	. 2 |- ( ( A e. C /\ E. y e. D ch ) -> E. x e. C E. y e. D ph )
8	4, 7	syl 17	1 |- ( ( A e. C /\ B e. D /\ ps ) -> E. x e. C E. y e. D ph )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-v 3202

This theorem is referenced by:  rspc3ev  3326  opelxp  5146  f1prex  6539  rspceov  6692  erov  7844  ralxpmap  7907  2dom  8029  elfiun  8336  dffi3  8337  ixpiunwdom  8496  1re  10039  hashdmpropge2  13265  wrdl2exs2  13690  ello12r  14248  ello1d  14254  elo12r  14259  o1lo1  14268  addcn2  14324  mulcn2  14326  bezoutlem3  15258  bezout  15260  pythagtriplem18  15537  pczpre  15552  pcdiv  15557  4sqlem3  15654  4sqlem4  15656  4sqlem12  15660  vdwlem1  15685  vdwlem6  15690  vdwlem8  15692  vdwlem12  15696  vdwlem13  15697  0ram  15724  ramz2  15728  sgrp2rid2ex  17414  pmtr3ncom  17895  psgnunilem1  17913  irredn0  18703  isnzr2  19263  hausnei2  21157  cnhaus  21158  dishaus  21186  ordthauslem  21187  txuni2  21368  xkoopn  21392  txopn  21405  txdis  21435  txdis1cn  21438  pthaus  21441  txhaus  21450  tx1stc  21453  xkohaus  21456  regr1lem  21542  qustgplem  21924  methaus  22325  met2ndci  22327  metnrmlem3  22664  elplyr  23957  aaliou2b  24096  aaliou3lem9  24105  2sqlem2  25143  2sqlem8  25151  2sqlem11  25154  2sqb  25157  pntibnd  25282  legov  25480  iscgrad  25703  f1otrge  25752  axsegconlem1  25797  axsegcon  25807  axpaschlem  25820  axlowdimlem6  25827  axlowdim1  25839  axlowdim2  25840  axeuclidlem  25842  structgrssvtxlemOLD  25915  umgrvad2edg  26105  wwlksnwwlksnon  26810  upgr4cycl4dv4e  27045  3cyclfrgrrn1  27149  4cycl2vnunb  27154  br8d  29422  lt2addrd  29516  xlt2addrd  29523  xrnarchi  29738  txomap  29901  tpr2rico  29958  qqhval2  30026  elsx  30257  isanmbfm  30318  br2base  30331  dya2iocnrect  30343  connpconn  31217  br8  31646  br4  31648  fprb  31669  brsegle  32215  hilbert1.1  32261  nn0prpwlem  32317  knoppndvlem21  32523  poimirlem1  33410  itg2addnclem3  33463  cntotbnd  33595  smprngopr  33851  3dim2  34754  llni2  34798  lvoli3  34863  lvoli2  34867  islinei  35026  psubspi2N  35034  elpaddri  35088  eldioph2lem1  37323  diophin  37336  fphpdo  37381  irrapxlem3  37388  irrapxlem4  37389  pellexlem6  37398  pell1234qrreccl  37418  pell1234qrmulcl  37419  pell1234qrdich  37425  pell1qr1  37435  pellqrexplicit  37441  rmxycomplete  37482  dgraalem  37715  clsk3nimkb  38338  fourierdlem64  40387  rspceaov  41277  6gbe  41659  7gbow  41660  8gbe  41661  9gbo  41662  11gbo  41663  prelspr  41736  modn0mul  42315  elbigo2r  42347