Theorem rspc2v 3612

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052

This theorem is referenced by:  rspc2va  3613  rspc3v  3617  rspc6v  3622  disji2  5103  f1veqaeq  7248  isorel  7318  isosolem  7339  oveqrspc2v  7430  fovcld  7532  caovclg  7597  caovcomg  7600  caofidlcan  7707  resf1extb  7928  smoel  8372  fiint  9336  fiintOLD  9337  dffi3  9441  ltordlem  11760  seqhomo  14065  cshf1  14826  climcn2  15607  drsdir  18312  tsrlin  18593  dirge  18611  mgmhmlin  18675  issubmgm2  18679  mhmlin  18769  issubg2  19122  nsgbi  19138  ghmlin  19202  efgi  19698  efgred  19727  rglcom4d  20169  irredmul  20387  issubrng2  20516  issubrg2  20550  abvmul  20779  abvtri  20780  lmodlema  20820  islmodd  20821  rmodislmodlem  20884  rmodislmod  20885  lmhmlin  20991  lbsind  21036  rnglidlmcl  21175  ipcj  21592  obsip  21679  mplcoe5lem  21995  matecl  22361  dmatelnd  22432  scmateALT  22448  mdetdiaglem  22534  mdetdiagid  22536  pmatcoe1fsupp  22637  m2cpminvid2lem  22690  inopn  22835  basis1  22886  basis2  22887  iscldtop  23031  hausnei  23264  t1sep2  23305  nconnsubb  23359  r0sep  23684  fbasssin  23772  fcfneii  23973  ustssel  24142  xmeteq0  24275  tngngp3  24593  nmvs  24613  cncfi  24836  c1lip1  25952  aalioulem3  26292  logltb  26559  cvxcl  26945  2sqlem8  27387  nocvxminlem  27739  madebday  27855  negsproplem1  27977  negsprop  27984  axtgcgrrflx  28387  axtgsegcon  28389  axtg5seg  28390  axtgbtwnid  28391  axtgpasch  28392  axtgcont1  28393  axtgupdim2  28396  axtgeucl  28397  isperp2d  28641  f1otrgds  28794  brbtwn2  28830  axcontlem3  28891  axcontlem9  28897  axcontlem10  28898  upgrwlkdvdelem  29664  conngrv2edg  30122  frgrwopreglem5ALT  30249  ablocom  30475  nvs  30590  nvtri  30597  phpar2  30750  phpar  30751  shaddcl  31144  shmulcl  31145  cnopc  31840  unop  31842  hmop  31849  cnfnc  31857  adj1  31860  hstel2  32146  stj  32162  stcltr1i  32201  mddmdin0i  32358  cdj3lem1  32361  cdj3lem2b  32364  disji2f  32504  disjif2  32508  disjxpin  32515  isoun  32625  archirng  33132  archiexdiv  33134  slmdlema  33146  inelcarsg  34289  sibfof  34318  breprexplema  34608  axtgupdim2ALTV  34646  pconncn  35192  ivthALT  36299  poimirlem32  37622  ismtycnv  37772  ismtyima  37773  ismtyres  37778  bfplem1  37792  bfplem2  37793  ghomlinOLD  37858  rngohomadd  37939  rngohommul  37940  crngocom  37971  idladdcl  37989  idllmulcl  37990  idlrmulcl  37991  pridl  38007  ispridlc  38040  pridlc  38041  dmnnzd  38045  oposlem  39146  omllaw  39207  hlsuprexch  39346  lautle  40049  ltrnu  40086  tendovalco  40730  sticksstones1  42105  sticksstones2  42106  ntrkbimka  44009  relprel  44924  mullimc  45593  mullimcf  45600  lptre2pt  45617  fourierdlem54  46137  fcoresf1  47046  faovcl  47177  icceuelpartlem  47397  iccpartnel  47400  fargshiftf1  47403  sprsymrelfolem2  47455  reuopreuprim  47488  isubgr3stgrlem6  47931  isthincd2lem2  49269