Theorem rspc2v 3572

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1522   ∈ wcel 2081  ∀wral 3105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-v 3439

This theorem is referenced by:  rspc2va  3573  rspc3v  3575  disji2  4946  f1veqaeq  6880  isorel  6942  isosolem  6963  oveqrspc2v  7043  fovcl  7135  caovclg  7196  caovcomg  7199  smoel  7849  fiint  8641  dffi3  8741  ltordlem  11013  seqhomo  13267  cshf1  14008  climcn2  14783  drsdir  17374  tsrlin  17658  dirge  17676  mhmlin  17781  issubg2  18048  nsgbi  18064  ghmlin  18104  efgi  18572  efgred  18601  irredmul  19149  issubrg2  19245  abvmul  19290  abvtri  19291  lmodlema  19329  islmodd  19330  rmodislmodlem  19391  rmodislmod  19392  lmhmlin  19497  lbsind  19542  mplcoe5lem  19935  ipcj  20460  obsip  20547  matecl  20718  dmatelnd  20789  scmateALT  20805  mdetdiaglem  20891  mdetdiagid  20893  pmatcoe1fsupp  20993  m2cpminvid2lem  21046  inopn  21191  basis1  21242  basis2  21243  iscldtop  21387  hausnei  21620  t1sep2  21661  nconnsubb  21715  r0sep  22040  fbasssin  22128  fcfneii  22329  ustssel  22497  xmeteq0  22631  tngngp3  22948  nmvs  22968  cncfi  23185  c1lip1  24277  aalioulem3  24606  logltb  24864  cvxcl  25244  2sqlem8  25684  axtgcgrrflx  25930  axtgsegcon  25932  axtg5seg  25933  axtgbtwnid  25934  axtgpasch  25935  axtgcont1  25936  axtgupdim2  25939  axtgeucl  25940  isperp2d  26184  f1otrgds  26338  brbtwn2  26374  axcontlem3  26435  axcontlem9  26441  axcontlem10  26442  upgrwlkdvdelem  27204  conngrv2edg  27661  frgrwopreglem5ALT  27793  ablocom  28016  nvs  28131  nvtri  28138  phpar2  28291  phpar  28292  shaddcl  28685  shmulcl  28686  cnopc  29381  unop  29383  hmop  29390  cnfnc  29398  adj1  29401  hstel2  29687  stj  29703  stcltr1i  29742  mddmdin0i  29899  cdj3lem1  29902  cdj3lem2b  29905  disji2f  30017  disjif2  30021  disjxpin  30028  fovcld  30075  isoun  30125  archirng  30455  archiexdiv  30457  slmdlema  30469  inelcarsg  31186  sibfof  31215  breprexplema  31518  axtgupdim2ALTV  31556  pconncn  32079  nocvxminlem  32856  ivthALT  33292  poimirlem32  34455  ismtycnv  34612  ismtyima  34613  ismtyres  34618  bfplem1  34632  bfplem2  34633  ghomlinOLD  34698  rngohomadd  34779  rngohommul  34780  crngocom  34811  idladdcl  34829  idllmulcl  34830  idlrmulcl  34831  pridl  34847  ispridlc  34880  pridlc  34881  dmnnzd  34885  oposlem  35849  omllaw  35910  hlsuprexch  36048  lautle  36751  ltrnu  36788  tendovalco  37432  ntrkbimka  39873  mullimc  41439  mullimcf  41446  lptre2pt  41463  fourierdlem54  41987  faovcl  42915  icceuelpartlem  43077  iccpartnel  43080  fargshiftf1  43083  sprsymrelfolem2  43137  reuopreuprim  43170  mgmhmlin  43535  issubmgm2  43539