Theorem rspc2v 3592

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080

This theorem is referenced by:  rspc2va  3593  rspc3v  3597  rspc6v  3602  disji2  5093  f1veqaeq  7254  isorel  7324  isosolem  7345  oveqrspc2v  7437  fovcld  7537  caovclg  7602  caovcomg  7605  caofidlcan  7712  resf1extb  7927  smoel  8343  fiint  9282  dffi3  9387  ltordlem  11734  seqhomo  14081  cshf1  14843  climcn2  15640  drsdir  18353  tsrlin  18636  dirge  18654  mgmhmlin  18752  issubmgm2  18756  mhmlin  18846  issubg2  19203  nsgbi  19218  ghmlin  19286  efgi  19784  efgred  19813  rglcom4d  20288  irredmul  20507  issubrng2  20657  issubrg2  20691  abvmul  20924  abvtri  20925  lmodlema  20986  islmodd  20987  rmodislmodlem  21050  rmodislmod  21051  lmhmlin  21156  lbsind  21201  rnglidlmcl  21341  unichnlidl  21362  ipcj  21784  obsip  21871  mplcoe5lem  22190  matecl  22582  dmatelnd  22653  scmateALT  22669  mdetdiaglem  22755  mdetdiagid  22757  pmatcoe1fsupp  22858  m2cpminvid2lem  22911  inopn  23056  basis1  23107  basis2  23108  iscldtop  23252  hausnei  23485  t1sep2  23526  nconnsubb  23580  r0sep  23905  fbasssin  23993  fcfneii  24194  ustssel  24363  xmeteq0  24495  tngngp3  24813  nmvs  24833  cncfi  25053  c1lip1  26156  aalioulem3  26497  logltb  26765  cvxcl  27149  2sqlem8  27590  nocvxminlem  27947  madebday  28093  negsproplem1  28221  negsprop  28228  axtgcgrrflx  28731  axtgsegcon  28733  axtg5seg  28734  axtgbtwnid  28735  axtgpasch  28736  axtgcont1  28737  axtgupdim2  28740  axtgeucl  28741  isperp2d  28996  f1otrgds  29218  brbtwn2  29255  axcontlem3  29316  axcontlem9  29322  axcontlem10  29323  upgrwlkdvdelem  30085  conngrv2edg  30546  frgrwopreglem5ALT  30673  ablocom  30900  nvs  31015  nvtri  31022  phpar2  31175  phpar  31176  shaddcl  31569  shmulcl  31570  cnopc  32265  unop  32267  hmop  32274  cnfnc  32282  adj1  32285  hstel2  32571  stj  32587  stcltr1i  32626  mddmdin0i  32783  cdj3lem1  32786  cdj3lem2b  32789  disji2f  32922  disjif2  32926  disjxpin  32933  isoun  33047  archirng  33508  archiexdiv  33510  slmdlema  33523  inelcarsg  34701  sibfof  34730  breprexplema  35017  axtgupdim2ALTV  35055  pconncn  35716  ivthALT  36866  poimirlem32  38323  ismtycnv  38473  ismtyima  38474  ismtyres  38479  bfplem1  38493  bfplem2  38494  ghomlinOLD  38559  rngohomadd  38640  rngohommul  38641  crngocom  38672  idladdcl  38690  idllmulcl  38691  idlrmulcl  38692  pridl  38708  ispridlc  38741  pridlc  38742  dmnnzd  38746  oposlem  39976  omllaw  40037  hlsuprexch  40175  lautle  40878  ltrnu  40915  tendovalco  41559  sticksstones1  42933  sticksstones2  42934  ntrkbimka  44784  relprel  45680  mullimc  46352  mullimcf  46359  lptre2pt  46374  fourierdlem54  46894  fcoresf1  47826  faovcl  47957  icceuelpartlem  48204  iccpartnel  48207  fargshiftf1  48210  sprsymrelfolem2  48262  reuopreuprim  48295  isubgr3stgrlem6  48756  idomnzd  49131  isthincd2lem2  50233