Theorem rspc2v 3633

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.)

Hypotheses

Ref	Expression
rspc2v.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
rspc2v.2	⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))

Assertion

Ref	Expression
rspc2v	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝐷,𝑦   𝜒,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑦)   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem rspc2v

Step	Hyp	Ref	Expression
1		rspc2v.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2	1	ralbidv 3178	. . 3 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑦 ∈ 𝐷 𝜒))
3	2	rspcv 3618	. 2 ⊢ (𝐴 ∈ 𝐶 → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐷 𝜒))
4		rspc2v.2	. . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
5	4	rspcv 3618	. 2 ⊢ (𝐵 ∈ 𝐷 → (∀𝑦 ∈ 𝐷 𝜒 → 𝜓))
6	3, 5	sylan9 507	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062

This theorem is referenced by:  rspc2va  3634  rspc3v  3638  rspc6v  3643  disji2  5127  f1veqaeq  7277  isorel  7346  isosolem  7367  oveqrspc2v  7458  fovcld  7560  caovclg  7625  caovcomg  7628  caofidlcan  7735  resf1extb  7956  smoel  8400  fiint  9366  fiintOLD  9367  dffi3  9471  ltordlem  11788  seqhomo  14090  cshf1  14848  climcn2  15629  drsdir  18348  tsrlin  18630  dirge  18648  mgmhmlin  18712  issubmgm2  18716  mhmlin  18806  issubg2  19159  nsgbi  19175  ghmlin  19239  efgi  19737  efgred  19766  rglcom4d  20208  irredmul  20429  issubrng2  20558  issubrg2  20592  abvmul  20822  abvtri  20823  lmodlema  20863  islmodd  20864  rmodislmodlem  20927  rmodislmod  20928  lmhmlin  21034  lbsind  21079  rnglidlmcl  21226  ipcj  21652  obsip  21741  mplcoe5lem  22057  matecl  22431  dmatelnd  22502  scmateALT  22518  mdetdiaglem  22604  mdetdiagid  22606  pmatcoe1fsupp  22707  m2cpminvid2lem  22760  inopn  22905  basis1  22957  basis2  22958  iscldtop  23103  hausnei  23336  t1sep2  23377  nconnsubb  23431  r0sep  23756  fbasssin  23844  fcfneii  24045  ustssel  24214  xmeteq0  24348  tngngp3  24677  nmvs  24697  cncfi  24920  c1lip1  26036  aalioulem3  26376  logltb  26642  cvxcl  27028  2sqlem8  27470  nocvxminlem  27822  madebday  27938  negsproplem1  28060  negsprop  28067  axtgcgrrflx  28470  axtgsegcon  28472  axtg5seg  28473  axtgbtwnid  28474  axtgpasch  28475  axtgcont1  28476  axtgupdim2  28479  axtgeucl  28480  isperp2d  28724  f1otrgds  28877  brbtwn2  28920  axcontlem3  28981  axcontlem9  28987  axcontlem10  28988  upgrwlkdvdelem  29756  conngrv2edg  30214  frgrwopreglem5ALT  30341  ablocom  30567  nvs  30682  nvtri  30689  phpar2  30842  phpar  30843  shaddcl  31236  shmulcl  31237  cnopc  31932  unop  31934  hmop  31941  cnfnc  31949  adj1  31952  hstel2  32238  stj  32254  stcltr1i  32293  mddmdin0i  32450  cdj3lem1  32453  cdj3lem2b  32456  disji2f  32590  disjif2  32594  disjxpin  32601  isoun  32711  archirng  33195  archiexdiv  33197  slmdlema  33209  inelcarsg  34313  sibfof  34342  breprexplema  34645  axtgupdim2ALTV  34683  pconncn  35229  ivthALT  36336  poimirlem32  37659  ismtycnv  37809  ismtyima  37810  ismtyres  37815  bfplem1  37829  bfplem2  37830  ghomlinOLD  37895  rngohomadd  37976  rngohommul  37977  crngocom  38008  idladdcl  38026  idllmulcl  38027  idlrmulcl  38028  pridl  38044  ispridlc  38077  pridlc  38078  dmnnzd  38082  oposlem  39183  omllaw  39244  hlsuprexch  39383  lautle  40086  ltrnu  40123  tendovalco  40767  sticksstones1  42147  sticksstones2  42148  ntrkbimka  44051  relprel  44972  mullimc  45631  mullimcf  45638  lptre2pt  45655  fourierdlem54  46175  fcoresf1  47081  faovcl  47212  icceuelpartlem  47422  iccpartnel  47425  fargshiftf1  47428  sprsymrelfolem2  47480  reuopreuprim  47513  isubgr3stgrlem6  47938  isthincd2lem2  49084