Theorem rspc2v 3601

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086

This theorem is referenced by:  rspc2va  3602  rspc3v  3606  rspc6v  3611  disji2  5097  f1veqaeq  7255  isorel  7325  isosolem  7346  oveqrspc2v  7438  fovcld  7538  caovclg  7603  caovcomg  7606  caofidlcan  7713  resf1extb  7931  smoel  8347  fiint  9286  dffi3  9391  ltordlem  11739  seqhomo  14085  cshf1  14847  climcn2  15644  drsdir  18358  tsrlin  18641  dirge  18659  mgmhmlin  18757  issubmgm2  18761  mhmlin  18851  issubg2  19208  nsgbi  19223  ghmlin  19291  efgi  19789  efgred  19818  rglcom4d  20293  irredmul  20511  issubrng2  20643  issubrg2  20677  abvmul  20902  abvtri  20903  lmodlema  20964  islmodd  20965  rmodislmodlem  21028  rmodislmod  21029  lmhmlin  21134  lbsind  21179  rnglidlmcl  21319  unichnlidl  21340  ipcj  21753  obsip  21840  mplcoe5lem  22159  matecl  22551  dmatelnd  22622  scmateALT  22638  mdetdiaglem  22724  mdetdiagid  22726  pmatcoe1fsupp  22827  m2cpminvid2lem  22880  inopn  23025  basis1  23076  basis2  23077  iscldtop  23221  hausnei  23454  t1sep2  23495  nconnsubb  23549  r0sep  23874  fbasssin  23962  fcfneii  24163  ustssel  24332  xmeteq0  24464  tngngp3  24782  nmvs  24802  cncfi  25022  c1lip1  26125  aalioulem3  26464  logltb  26731  cvxcl  27115  2sqlem8  27556  nocvxminlem  27913  madebday  28059  negsproplem1  28187  negsprop  28194  axtgcgrrflx  28697  axtgsegcon  28699  axtg5seg  28700  axtgbtwnid  28701  axtgpasch  28702  axtgcont1  28703  axtgupdim2  28706  axtgeucl  28707  isperp2d  28955  f1otrgds  29159  brbtwn2  29196  axcontlem3  29257  axcontlem9  29263  axcontlem10  29264  upgrwlkdvdelem  30026  conngrv2edg  30487  frgrwopreglem5ALT  30614  ablocom  30841  nvs  30956  nvtri  30963  phpar2  31116  phpar  31117  shaddcl  31510  shmulcl  31511  cnopc  32206  unop  32208  hmop  32215  cnfnc  32223  adj1  32226  hstel2  32512  stj  32528  stcltr1i  32567  mddmdin0i  32724  cdj3lem1  32727  cdj3lem2b  32730  disji2f  32863  disjif2  32867  disjxpin  32874  isoun  32988  archirng  33449  archiexdiv  33451  slmdlema  33464  inelcarsg  34646  sibfof  34675  breprexplema  34962  axtgupdim2ALTV  35000  pconncn  35615  ivthALT  36735  poimirlem32  38191  ismtycnv  38341  ismtyima  38342  ismtyres  38347  bfplem1  38361  bfplem2  38362  ghomlinOLD  38427  rngohomadd  38508  rngohommul  38509  crngocom  38540  idladdcl  38558  idllmulcl  38559  idlrmulcl  38560  pridl  38576  ispridlc  38609  pridlc  38610  dmnnzd  38614  oposlem  39846  omllaw  39907  hlsuprexch  40045  lautle  40748  ltrnu  40785  tendovalco  41429  sticksstones1  42803  sticksstones2  42804  ntrkbimka  44656  relprel  45552  mullimc  46224  mullimcf  46231  lptre2pt  46246  fourierdlem54  46766  fcoresf1  47695  faovcl  47826  icceuelpartlem  48073  iccpartnel  48076  fargshiftf1  48079  sprsymrelfolem2  48131  reuopreuprim  48164  isubgr3stgrlem6  48625  isthincd2lem2  50098