Theorem rspc2v 3526

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1637   ∈ wcel 2157  ∀wral 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-v 3404

This theorem is referenced by:  rspc2va  3527  rspc3v  3529  disji2  4839  f1veqaeq  6745  isorel  6807  isosolem  6828  oveqrspc2v  6908  fovcl  7002  caovclg  7063  caovcomg  7066  smoel  7700  fiint  8483  dffi3  8583  ltordlem  10845  seqhomo  13078  cshf1  13787  climcn2  14553  drsdir  17147  tsrlin  17431  dirge  17449  mhmlin  17554  issubg2  17818  nsgbi  17834  ghmlin  17874  efgi  18340  efgred  18369  irredmul  18918  issubrg2  19011  abvmul  19040  abvtri  19041  lmodlema  19079  islmodd  19080  rmodislmodlem  19141  rmodislmod  19142  lmhmlin  19249  lbsind  19294  mplcoe5lem  19683  ipcj  20196  obsip  20283  matecl  20449  dmatelnd  20521  scmateALT  20537  mdetdiaglem  20623  mdetdiagid  20625  pmatcoe1fsupp  20727  m2cpminvid2lem  20780  inopn  20925  basis1  20976  basis2  20977  iscldtop  21121  hausnei  21354  t1sep2  21395  nconnsubb  21448  r0sep  21773  fbasssin  21861  fcfneii  22062  ustssel  22230  xmeteq0  22364  tngngp3  22681  nmvs  22701  cncfi  22918  c1lip1  23984  aalioulem3  24313  logltb  24570  cvxcl  24935  2sqlem8  25375  axtgcgrrflx  25585  axtgsegcon  25587  axtg5seg  25588  axtgbtwnid  25589  axtgpasch  25590  axtgcont1  25591  axtgupdim2  25594  axtgeucl  25595  iscgrglt  25633  isperp2d  25835  f1otrgds  25973  brbtwn2  26009  axcontlem3  26070  axcontlem9  26076  axcontlem10  26077  upgrwlkdvdelem  26870  conngrv2edg  27378  frgrwopreglem5ALT  27507  ablocom  27741  nvs  27856  nvtri  27863  phpar2  28016  phpar  28017  shaddcl  28412  shmulcl  28413  cnopc  29110  unop  29112  hmop  29119  cnfnc  29127  adj1  29130  hstel2  29416  stj  29432  stcltr1i  29471  mddmdin0i  29628  cdj3lem1  29631  cdj3lem2b  29634  disji2f  29725  disjif2  29729  disjxpin  29736  fovcld  29777  isoun  29816  archirng  30077  archiexdiv  30079  slmdlema  30091  inelcarsg  30708  sibfof  30737  breprexplema  31043  axtgupdim2OLD  31081  pconncn  31538  nocvxminlem  32223  ivthALT  32660  poimirlem32  33760  ismtycnv  33918  ismtyima  33919  ismtyres  33924  bfplem1  33938  bfplem2  33939  ghomlinOLD  34004  rngohomadd  34085  rngohommul  34086  crngocom  34117  idladdcl  34135  idllmulcl  34136  idlrmulcl  34137  pridl  34153  ispridlc  34186  pridlc  34187  dmnnzd  34191  oposlem  34968  omllaw  35029  hlsuprexch  35167  lautle  35870  ltrnu  35907  tendovalco  36551  ntrkbimka  38841  mullimc  40333  mullimcf  40340  lptre2pt  40357  fourierdlem54  40861  faovcl  41794  icceuelpartlem  41951  iccpartnel  41954  fargshiftf1  41957  sprsymrelfolem2  42316  mgmhmlin  42359  issubmgm2  42363