Theorem rspc2v 3632

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059

This theorem is referenced by:  rspc2va  3633  rspc3v  3637  rspc6v  3642  disji2  5131  f1veqaeq  7276  isorel  7345  isosolem  7366  oveqrspc2v  7457  fovcld  7559  caovclg  7624  caovcomg  7627  smoel  8398  fiint  9363  fiintOLD  9364  dffi3  9468  ltordlem  11785  seqhomo  14086  cshf1  14844  climcn2  15625  drsdir  18359  tsrlin  18642  dirge  18660  mgmhmlin  18724  issubmgm2  18728  mhmlin  18818  issubg2  19171  nsgbi  19187  ghmlin  19251  efgi  19751  efgred  19780  rglcom4d  20228  irredmul  20445  issubrng2  20574  issubrg2  20608  abvmul  20838  abvtri  20839  lmodlema  20879  islmodd  20880  rmodislmodlem  20943  rmodislmod  20944  rmodislmodOLD  20945  lmhmlin  21051  lbsind  21096  rnglidlmcl  21243  ipcj  21669  obsip  21758  mplcoe5lem  22074  matecl  22446  dmatelnd  22517  scmateALT  22533  mdetdiaglem  22619  mdetdiagid  22621  pmatcoe1fsupp  22722  m2cpminvid2lem  22775  inopn  22920  basis1  22972  basis2  22973  iscldtop  23118  hausnei  23351  t1sep2  23392  nconnsubb  23446  r0sep  23771  fbasssin  23859  fcfneii  24060  ustssel  24229  xmeteq0  24363  tngngp3  24692  nmvs  24712  cncfi  24933  c1lip1  26050  aalioulem3  26390  logltb  26656  cvxcl  27042  2sqlem8  27484  nocvxminlem  27836  madebday  27952  negsproplem1  28074  negsprop  28081  axtgcgrrflx  28484  axtgsegcon  28486  axtg5seg  28487  axtgbtwnid  28488  axtgpasch  28489  axtgcont1  28490  axtgupdim2  28493  axtgeucl  28494  isperp2d  28738  f1otrgds  28891  brbtwn2  28934  axcontlem3  28995  axcontlem9  29001  axcontlem10  29002  upgrwlkdvdelem  29768  conngrv2edg  30223  frgrwopreglem5ALT  30350  ablocom  30576  nvs  30691  nvtri  30698  phpar2  30851  phpar  30852  shaddcl  31245  shmulcl  31246  cnopc  31941  unop  31943  hmop  31950  cnfnc  31958  adj1  31961  hstel2  32247  stj  32263  stcltr1i  32302  mddmdin0i  32459  cdj3lem1  32462  cdj3lem2b  32465  disji2f  32596  disjif2  32600  disjxpin  32607  isoun  32716  archirng  33177  archiexdiv  33179  slmdlema  33191  inelcarsg  34292  sibfof  34321  breprexplema  34623  axtgupdim2ALTV  34661  pconncn  35208  ivthALT  36317  poimirlem32  37638  ismtycnv  37788  ismtyima  37789  ismtyres  37794  bfplem1  37808  bfplem2  37809  ghomlinOLD  37874  rngohomadd  37955  rngohommul  37956  crngocom  37987  idladdcl  38005  idllmulcl  38006  idlrmulcl  38007  pridl  38023  ispridlc  38056  pridlc  38057  dmnnzd  38061  oposlem  39163  omllaw  39224  hlsuprexch  39363  lautle  40066  ltrnu  40103  tendovalco  40747  sticksstones1  42127  sticksstones2  42128  ntrkbimka  44027  mullimc  45571  mullimcf  45578  lptre2pt  45595  fourierdlem54  46115  fcoresf1  47018  faovcl  47149  icceuelpartlem  47359  iccpartnel  47362  fargshiftf1  47365  sprsymrelfolem2  47417  reuopreuprim  47450  isubgr3stgrlem6  47873  isthincd2lem2  48835