Theorem rspc2v 3537

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 3108	. . 3 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑦 ∈ 𝐷 𝜒))
3	2	rspcv 3522	. 2 ⊢ (𝐴 ∈ 𝐶 → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐷 𝜒))
4		rspc2v.2	. . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
5	4	rspcv 3522	. 2 ⊢ (𝐵 ∈ 𝐷 → (∀𝑦 ∈ 𝐷 𝜒 → 𝜓))
6	3, 5	sylan9 511	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2112  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056

This theorem is referenced by:  rspc2va  3538  rspc3v  3540  disji2  5021  f1veqaeq  7047  isorel  7113  isosolem  7134  oveqrspc2v  7218  fovcl  7316  caovclg  7378  caovcomg  7381  smoel  8075  fiint  8926  dffi3  9025  ltordlem  11322  seqhomo  13588  cshf1  14340  climcn2  15119  drsdir  17763  tsrlin  18045  dirge  18063  mhmlin  18179  issubg2  18512  nsgbi  18527  ghmlin  18581  efgi  19063  efgred  19092  irredmul  19681  issubrg2  19774  abvmul  19819  abvtri  19820  lmodlema  19858  islmodd  19859  rmodislmodlem  19920  rmodislmod  19921  lmhmlin  20026  lbsind  20071  ipcj  20550  obsip  20637  mplcoe5lem  20950  matecl  21276  dmatelnd  21347  scmateALT  21363  mdetdiaglem  21449  mdetdiagid  21451  pmatcoe1fsupp  21552  m2cpminvid2lem  21605  inopn  21750  basis1  21801  basis2  21802  iscldtop  21946  hausnei  22179  t1sep2  22220  nconnsubb  22274  r0sep  22599  fbasssin  22687  fcfneii  22888  ustssel  23057  xmeteq0  23190  tngngp3  23508  nmvs  23528  cncfi  23745  c1lip1  24848  aalioulem3  25181  logltb  25442  cvxcl  25821  2sqlem8  26261  axtgcgrrflx  26507  axtgsegcon  26509  axtg5seg  26510  axtgbtwnid  26511  axtgpasch  26512  axtgcont1  26513  axtgupdim2  26516  axtgeucl  26517  isperp2d  26761  f1otrgds  26914  brbtwn2  26950  axcontlem3  27011  axcontlem9  27017  axcontlem10  27018  upgrwlkdvdelem  27777  conngrv2edg  28232  frgrwopreglem5ALT  28359  ablocom  28583  nvs  28698  nvtri  28705  phpar2  28858  phpar  28859  shaddcl  29252  shmulcl  29253  cnopc  29948  unop  29950  hmop  29957  cnfnc  29965  adj1  29968  hstel2  30254  stj  30270  stcltr1i  30309  mddmdin0i  30466  cdj3lem1  30469  cdj3lem2b  30472  disji2f  30589  disjif2  30593  disjxpin  30600  fovcld  30648  isoun  30708  archirng  31115  archiexdiv  31117  slmdlema  31129  inelcarsg  31944  sibfof  31973  breprexplema  32276  axtgupdim2ALTV  32314  pconncn  32853  nocvxminlem  33658  madebday  33766  ivthALT  34210  poimirlem32  35495  ismtycnv  35646  ismtyima  35647  ismtyres  35652  bfplem1  35666  bfplem2  35667  ghomlinOLD  35732  rngohomadd  35813  rngohommul  35814  crngocom  35845  idladdcl  35863  idllmulcl  35864  idlrmulcl  35865  pridl  35881  ispridlc  35914  pridlc  35915  dmnnzd  35919  oposlem  36882  omllaw  36943  hlsuprexch  37081  lautle  37784  ltrnu  37821  tendovalco  38465  sticksstones1  39771  sticksstones2  39772  ntrkbimka  41266  mullimc  42775  mullimcf  42782  lptre2pt  42799  fourierdlem54  43319  fcoresf1  44178  faovcl  44307  icceuelpartlem  44503  iccpartnel  44506  fargshiftf1  44509  sprsymrelfolem2  44561  reuopreuprim  44594  mgmhmlin  44956  issubmgm2  44960  isthincd2lem2  45933