Theorem rspc2v 3322

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		nfv 1843	. 2 ⊢ Ⅎ𝑥𝜒
2		nfv 1843	. 2 ⊢ Ⅎ𝑦𝜓
3		rspc2v.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
4		rspc2v.2	. 2 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
5	1, 2, 3, 4	rspc2 3320	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202

This theorem is referenced by:  rspc2va  3323  rspc3v  3325  disji2  4636  f1veqaeq  6514  isorel  6576  isosolem  6597  oveqrspc2v  6673  fovcl  6765  caovclg  6826  caovcomg  6829  smoel  7457  fiint  8237  dffi3  8337  ltordlem  10553  seqhomo  12848  cshf1  13556  climcn2  14323  drsdir  16935  tsrlin  17219  dirge  17237  mhmlin  17342  issubg2  17609  nsgbi  17625  ghmlin  17665  efgi  18132  efgred  18161  irredmul  18709  issubrg2  18800  abvmul  18829  abvtri  18830  lmodlema  18868  islmodd  18869  rmodislmodlem  18930  rmodislmod  18931  lmhmlin  19035  lbsind  19080  mplcoe5lem  19467  ipcj  19979  obsip  20065  matecl  20231  dmatelnd  20302  scmateALT  20318  mdetdiaglem  20404  mdetdiagid  20406  pmatcoe1fsupp  20506  m2cpminvid2lem  20559  inopn  20704  basis1  20754  basis2  20755  iscldtop  20899  hausnei  21132  t1sep2  21173  nconnsubb  21226  r0sep  21551  fbasssin  21640  fcfneii  21841  ustssel  22009  xmeteq0  22143  tngngp3  22460  nmvs  22480  cncfi  22697  c1lip1  23760  aalioulem3  24089  logltb  24346  cvxcl  24711  2sqlem8  25151  axtgcgrrflx  25361  axtgsegcon  25363  axtg5seg  25364  axtgbtwnid  25365  axtgpasch  25366  axtgcont1  25367  axtgupdim2  25370  axtgeucl  25371  iscgrglt  25409  isperp2d  25611  f1otrgds  25749  brbtwn2  25785  axcontlem3  25846  axcontlem9  25852  axcontlem10  25853  upgrwlkdvdelem  26632  conngrv2edg  27055  frgrwopreglem5ALT  27186  ablocom  27402  nvs  27518  nvtri  27525  phpar2  27678  phpar  27679  shaddcl  28074  shmulcl  28075  cnopc  28772  unop  28774  hmop  28781  cnfnc  28789  adj1  28792  hstel2  29078  stj  29094  stcltr1i  29133  mddmdin0i  29290  cdj3lem1  29293  cdj3lem2b  29296  disji2f  29390  disjif2  29394  disjxpin  29401  fovcld  29440  isoun  29479  archirng  29742  archiexdiv  29744  slmdlema  29756  inelcarsg  30373  sibfof  30402  breprexplema  30708  axtgupdim2OLD  30746  pconncn  31206  nocvxminlem  31893  ivthALT  32330  poimirlem32  33441  ismtycnv  33601  ismtyima  33602  ismtyres  33607  bfplem1  33621  bfplem2  33622  ghomlinOLD  33687  rngohomadd  33768  rngohommul  33769  crngocom  33800  idladdcl  33818  idllmulcl  33819  idlrmulcl  33820  pridl  33836  ispridlc  33869  pridlc  33870  dmnnzd  33874  oposlem  34469  omllaw  34530  hlsuprexch  34667  lautle  35370  ltrnu  35407  tendovalco  36053  ntrkbimka  38336  mullimc  39848  mullimcf  39855  lptre2pt  39872  fourierdlem54  40377  faovcl  41280  icceuelpartlem  41371  iccpartnel  41374  fargshiftf1  41377  sprsymrelfolem2  41743  mgmhmlin  41786  issubmgm2  41790