Theorem rspc2v 3589

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2146  ∀wral 3079

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080

This theorem is used by:  rspc2va  3590  rspc3v  3594  rspc6v  3599  disji2  5089  f1veqaeq  7267  isorel  7341  isosolem  7362  oveqrspc2v  7454  fovcld  7554  caovclg  7620  caovcomg  7623  caofidlcan  7738  resf1extb  7953  smoel  8379  fiint  9329  dffi3  9433  ltordlem  11851  seqhomo  14202  cshf1  14972  climcn2  15772  drsdir  18488  tsrlin  18771  dirge  18789  mgmhmlin  18900  issubmgm2  18904  mhmlin  19000  issubg2  19364  nsgbi  19379  ghmlin  19447  efgi  19945  efgred  19974  rglcom4d  20449  irredmul  20671  issubrng2  20822  issubrg2  20856  abvmul  21090  abvtri  21091  lmodlema  21152  islmodd  21153  rmodislmodlem  21216  rmodislmod  21217  lmhmlin  21322  lbsind  21367  rnglidlmcl  21507  unichnlidl  21528  ipcj  21952  obsip  22039  mplcoe5lem  22360  matecl  22752  dmatelnd  22823  scmateALT  22839  mdetdiaglem  22925  mdetdiagid  22927  pmatcoe1fsupp  23031  m2cpminvid2lem  23084  inopn  23229  basis1  23280  basis2  23281  iscldtop  23425  hausnei  23658  t1sep2  23699  nconnsubb  23753  r0sep  24079  fbasssin  24167  fcfneii  24368  ustssel  24537  xmeteq0  24669  tngngp3  24987  nmvs  25007  cncfi  25227  c1lip1  26329  aalioulem3  26673  logltb  26940  cvxcl  27324  2sqlem8  27765  nocvxminlem  28152  madebday  28298  negsproplem1  28426  negsprop  28433  axtgcgrrflx  28936  axtgsegcon  28938  axtg5seg  28939  axtgbtwnid  28940  axtgpasch  28941  axtgcont1  28942  axtgupdim2  28945  axtgeucl  28946  isperp2d  29203  f1otrgds  29458  brbtwn2  29495  axcontlem3  29556  axcontlem9  29562  axcontlem10  29563  upgrwlkdvdelem  30334  conngrv2edg  30808  frgrwopreglem5ALT  30935  ablocom  31162  nvs  31277  nvtri  31284  phpar2  31437  phpar  31438  shaddcl  31831  shmulcl  31832  cnopc  32527  unop  32529  hmop  32536  cnfnc  32544  adj1  32547  hstel2  32833  stj  32849  stcltr1i  32888  mddmdin0i  33045  cdj3lem1  33048  cdj3lem2b  33051  disji2f  33225  disjif2  33229  disjxpin  33236  isoun  33349  archirng  33802  archiexdiv  33804  slmdlema  33817  inelcarsg  34996  sibfof  35025  breprexplema  35312  axtgupdim2ALTV  35350  pconncn  36110  ivthALT  37250  poimirlem32  38710  ismtycnv  38876  ismtyima  38877  ismtyres  38882  bfplem1  38896  bfplem2  38897  ghomlinOLD  38962  rngohomadd  39043  rngohommul  39044  crngocom  39075  idladdcl  39093  idllmulcl  39094  idlrmulcl  39095  pridl  39111  ispridlc  39144  pridlc  39145  dmnnzd  39149  oposlem  40379  omllaw  40440  hlsuprexch  40578  lautle  41281  ltrnu  41318  tendovalco  41962  sticksstones1  43336  sticksstones2  43337  ntrkbimka  45178  relprel  46080  mullimc  46767  mullimcf  46774  lptre2pt  46789  fourierdlem54  47309  fcoresf1  48278  faovcl  48409  icceuelpartlem  48656  iccpartnel  48659  fargshiftf1  48662  sprsymrelfolem2  48714  reuopreuprim  48747  isubgr3stgrlem6  49208  idomnzd  49582  isthincd2lem2  50709