Theorem rspc2v 3292

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

Syntax hints:   → wi 4   ↔ wb 194   ∧ wa 382   = wceq 1474   ∈ wcel 1976  ∀wral 2895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-v 3174

This theorem is referenced by:  rspc2va  3293  rspc3v  3295  disji2  4563  f1veqaeq  6395  isorel  6453  isosolem  6474  oveqrspc2v  6549  fovcl  6640  caovclg  6701  caovcomg  6704  smoel  7321  fiint  8099  dffi3  8197  ltordlem  10404  seqhomo  12667  cshf1  13355  climcn2  14119  drsdir  16706  tsrlin  16990  dirge  17008  mhmlin  17113  issubg2  17380  nsgbi  17396  ghmlin  17436  efgi  17903  efgred  17932  irredmul  18480  issubrg2  18571  abvmul  18600  abvtri  18601  lmodlema  18639  islmodd  18640  lmhmlin  18804  lbsind  18849  mplcoe5lem  19236  ipcj  19745  obsip  19831  matecl  19997  dmatelnd  20068  scmateALT  20084  mdetdiaglem  20170  mdetdiagid  20172  pmatcoe1fsupp  20272  m2cpminvid2lem  20325  inopn  20476  basis1  20512  basis2  20513  iscldtop  20656  hausnei  20889  t1sep2  20930  nconsubb  20983  r0sep  21308  fbasssin  21397  fcfneii  21598  ustssel  21766  xmeteq0  21900  tngngp3  22217  nmvs  22237  cncfi  22452  c1lip1  23508  aalioulem3  23837  logltb  24094  cvxcl  24455  2sqlem8  24895  axtgcgrrflx  25105  axtgsegcon  25107  axtg5seg  25108  axtgbtwnid  25109  axtgpasch  25110  axtgcont1  25111  axtgupdim2  25114  axtgeucl  25115  iscgrglt  25154  isperp2d  25356  f1otrgds  25494  brbtwn2  25530  axcontlem3  25591  axcontlem9  25597  axcontlem10  25598  fargshiftf1  25958  ablocom  26579  nvs  26695  nvtri  26702  phpar2  26855  phpar  26856  shaddcl  27251  shmulcl  27252  cnopc  27949  unop  27951  hmop  27958  cnfnc  27966  adj1  27969  hstel2  28255  stj  28271  stcltr1i  28310  mddmdin0i  28467  cdj3lem1  28470  cdj3lem2b  28473  disji2f  28565  disjif2  28569  disjxpin  28576  fovcld  28613  isoun  28655  archirng  28866  archiexdiv  28868  slmdlema  28880  inelcarsg  29493  sibfof  29522  axtgupdim2OLD  29792  pconcn  30253  nocvxminlem  30882  nofulllem5  30898  ivthALT  31293  poimirlem32  32394  ismtycnv  32554  ismtyima  32555  ismtyres  32560  bfplem1  32574  bfplem2  32575  ghomlinOLD  32640  rngohomadd  32721  rngohommul  32722  crngocom  32753  idladdcl  32771  idllmulcl  32772  idlrmulcl  32773  pridl  32789  ispridlc  32822  pridlc  32823  dmnnzd  32827  oposlem  33270  omllaw  33331  hlsuprexch  33468  lautle  34171  ltrnu  34208  tendovalco  34854  ntrkbimka  37139  mullimc  38466  mullimcf  38473  lptre2pt  38490  fourierdlem54  38836  faovcl  39713  icceuelpartlem  39757  iccpartnel  39760  upgrwlkdvdelem  40923  conngrv2edg  41343  frgr2wwlkeqm  41477  mgmhmlin  41557  issubmgm2  41561