Theorem rspc2v 3633

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-ral 3143

This theorem is referenced by:  rspc2va  3634  rspc3v  3636  disji2  5048  f1veqaeq  7015  isorel  7079  isosolem  7100  oveqrspc2v  7183  fovcl  7279  caovclg  7340  caovcomg  7343  smoel  7997  fiint  8795  dffi3  8895  ltordlem  11165  seqhomo  13418  cshf1  14172  climcn2  14949  drsdir  17545  tsrlin  17829  dirge  17847  mhmlin  17963  issubg2  18294  nsgbi  18309  ghmlin  18363  efgi  18845  efgred  18874  irredmul  19459  issubrg2  19555  abvmul  19600  abvtri  19601  lmodlema  19639  islmodd  19640  rmodislmodlem  19701  rmodislmod  19702  lmhmlin  19807  lbsind  19852  mplcoe5lem  20248  ipcj  20778  obsip  20865  matecl  21034  dmatelnd  21105  scmateALT  21121  mdetdiaglem  21207  mdetdiagid  21209  pmatcoe1fsupp  21309  m2cpminvid2lem  21362  inopn  21507  basis1  21558  basis2  21559  iscldtop  21703  hausnei  21936  t1sep2  21977  nconnsubb  22031  r0sep  22356  fbasssin  22444  fcfneii  22645  ustssel  22814  xmeteq0  22948  tngngp3  23265  nmvs  23285  cncfi  23502  c1lip1  24594  aalioulem3  24923  logltb  25183  cvxcl  25562  2sqlem8  26002  axtgcgrrflx  26248  axtgsegcon  26250  axtg5seg  26251  axtgbtwnid  26252  axtgpasch  26253  axtgcont1  26254  axtgupdim2  26257  axtgeucl  26258  isperp2d  26502  f1otrgds  26655  brbtwn2  26691  axcontlem3  26752  axcontlem9  26758  axcontlem10  26759  upgrwlkdvdelem  27517  conngrv2edg  27974  frgrwopreglem5ALT  28101  ablocom  28325  nvs  28440  nvtri  28447  phpar2  28600  phpar  28601  shaddcl  28994  shmulcl  28995  cnopc  29690  unop  29692  hmop  29699  cnfnc  29707  adj1  29710  hstel2  29996  stj  30012  stcltr1i  30051  mddmdin0i  30208  cdj3lem1  30211  cdj3lem2b  30214  disji2f  30327  disjif2  30331  disjxpin  30338  fovcld  30385  isoun  30437  archirng  30817  archiexdiv  30819  slmdlema  30831  inelcarsg  31569  sibfof  31598  breprexplema  31901  axtgupdim2ALTV  31939  pconncn  32471  nocvxminlem  33247  ivthALT  33683  poimirlem32  34939  ismtycnv  35095  ismtyima  35096  ismtyres  35101  bfplem1  35115  bfplem2  35116  ghomlinOLD  35181  rngohomadd  35262  rngohommul  35263  crngocom  35294  idladdcl  35312  idllmulcl  35313  idlrmulcl  35314  pridl  35330  ispridlc  35363  pridlc  35364  dmnnzd  35368  oposlem  36333  omllaw  36394  hlsuprexch  36532  lautle  37235  ltrnu  37272  tendovalco  37916  ntrkbimka  40408  mullimc  41917  mullimcf  41924  lptre2pt  41941  fourierdlem54  42465  faovcl  43419  icceuelpartlem  43615  iccpartnel  43618  fargshiftf1  43621  sprsymrelfolem2  43675  reuopreuprim  43708  mgmhmlin  44073  issubmgm2  44077