Theorem rspc2v 3587

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  rspc2va  3588  rspc3v  3592  rspc6v  3597  disji2  5087  f1veqaeq  7254  isorel  7328  isosolem  7349  oveqrspc2v  7441  fovcld  7541  caovclg  7607  caovcomg  7610  caofidlcan  7717  resf1extb  7932  smoel  8350  fiint  9297  dffi3  9402  ltordlem  11764  seqhomo  14114  cshf1  14882  climcn2  15681  drsdir  18391  tsrlin  18674  dirge  18692  mgmhmlin  18802  issubmgm2  18806  mhmlin  18902  issubg2  19266  nsgbi  19281  ghmlin  19349  efgi  19847  efgred  19876  rglcom4d  20351  irredmul  20571  issubrng2  20721  issubrg2  20755  abvmul  20988  abvtri  20989  lmodlema  21050  islmodd  21051  rmodislmodlem  21114  rmodislmod  21115  lmhmlin  21220  lbsind  21265  rnglidlmcl  21405  unichnlidl  21426  ipcj  21848  obsip  21935  mplcoe5lem  22256  matecl  22648  dmatelnd  22719  scmateALT  22735  mdetdiaglem  22821  mdetdiagid  22823  pmatcoe1fsupp  22927  m2cpminvid2lem  22980  inopn  23125  basis1  23176  basis2  23177  iscldtop  23321  hausnei  23554  t1sep2  23595  nconnsubb  23649  r0sep  23975  fbasssin  24063  fcfneii  24264  ustssel  24433  xmeteq0  24565  tngngp3  24883  nmvs  24903  cncfi  25123  c1lip1  26225  aalioulem3  26571  logltb  26838  cvxcl  27222  2sqlem8  27663  nocvxminlem  28020  madebday  28166  negsproplem1  28294  negsprop  28301  axtgcgrrflx  28804  axtgsegcon  28806  axtg5seg  28807  axtgbtwnid  28808  axtgpasch  28809  axtgcont1  28810  axtgupdim2  28813  axtgeucl  28814  isperp2d  29071  f1otrgds  29326  brbtwn2  29363  axcontlem3  29424  axcontlem9  29430  axcontlem10  29431  upgrwlkdvdelem  30202  conngrv2edg  30676  frgrwopreglem5ALT  30803  ablocom  31030  nvs  31145  nvtri  31152  phpar2  31305  phpar  31306  shaddcl  31699  shmulcl  31700  cnopc  32395  unop  32397  hmop  32404  cnfnc  32412  adj1  32415  hstel2  32701  stj  32717  stcltr1i  32756  mddmdin0i  32913  cdj3lem1  32916  cdj3lem2b  32919  disji2f  33051  disjif2  33055  disjxpin  33062  isoun  33175  archirng  33629  archiexdiv  33631  slmdlema  33644  inelcarsg  34823  sibfof  34852  breprexplema  35139  axtgupdim2ALTV  35177  pconncn  35804  ivthALT  36955  poimirlem32  38402  ismtycnv  38553  ismtyima  38554  ismtyres  38559  bfplem1  38573  bfplem2  38574  ghomlinOLD  38639  rngohomadd  38720  rngohommul  38721  crngocom  38752  idladdcl  38770  idllmulcl  38771  idlrmulcl  38772  pridl  38788  ispridlc  38821  pridlc  38822  dmnnzd  38826  oposlem  40056  omllaw  40117  hlsuprexch  40255  lautle  40958  ltrnu  40995  tendovalco  41639  sticksstones1  43013  sticksstones2  43014  ntrkbimka  44879  relprel  45775  mullimc  46447  mullimcf  46454  lptre2pt  46469  fourierdlem54  46989  fcoresf1  47958  faovcl  48089  icceuelpartlem  48336  iccpartnel  48339  fargshiftf1  48342  sprsymrelfolem2  48394  reuopreuprim  48427  isubgr3stgrlem6  48888  idomnzd  49262  isthincd2lem2  50362