Theorem rspc2v 3623

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063

This theorem is referenced by:  rspc2va  3624  rspc3v  3628  rspc6v  3632  disji2  5131  f1veqaeq  7256  isorel  7323  isosolem  7344  oveqrspc2v  7436  fovcld  7536  caovclg  7599  caovcomg  7602  smoel  8360  fiint  9324  dffi3  9426  ltordlem  11739  seqhomo  14015  cshf1  14760  climcn2  15537  drsdir  18255  tsrlin  18538  dirge  18556  mhmlin  18679  issubg2  19021  nsgbi  19037  ghmlin  19097  efgi  19587  efgred  19616  rglcom4d  20034  irredmul  20243  issubrg2  20339  abvmul  20437  abvtri  20438  lmodlema  20476  islmodd  20477  rmodislmodlem  20539  rmodislmod  20540  rmodislmodOLD  20541  lmhmlin  20646  lbsind  20691  ipcj  21187  obsip  21276  mplcoe5lem  21594  matecl  21927  dmatelnd  21998  scmateALT  22014  mdetdiaglem  22100  mdetdiagid  22102  pmatcoe1fsupp  22203  m2cpminvid2lem  22256  inopn  22401  basis1  22453  basis2  22454  iscldtop  22599  hausnei  22832  t1sep2  22873  nconnsubb  22927  r0sep  23252  fbasssin  23340  fcfneii  23541  ustssel  23710  xmeteq0  23844  tngngp3  24173  nmvs  24193  cncfi  24410  c1lip1  25514  aalioulem3  25847  logltb  26108  cvxcl  26489  2sqlem8  26929  nocvxminlem  27279  madebday  27394  negsproplem1  27502  negsprop  27509  axtgcgrrflx  27713  axtgsegcon  27715  axtg5seg  27716  axtgbtwnid  27717  axtgpasch  27718  axtgcont1  27719  axtgupdim2  27722  axtgeucl  27723  isperp2d  27967  f1otrgds  28120  brbtwn2  28163  axcontlem3  28224  axcontlem9  28230  axcontlem10  28231  upgrwlkdvdelem  28993  conngrv2edg  29448  frgrwopreglem5ALT  29575  ablocom  29801  nvs  29916  nvtri  29923  phpar2  30076  phpar  30077  shaddcl  30470  shmulcl  30471  cnopc  31166  unop  31168  hmop  31175  cnfnc  31183  adj1  31186  hstel2  31472  stj  31488  stcltr1i  31527  mddmdin0i  31684  cdj3lem1  31687  cdj3lem2b  31690  disji2f  31808  disjif2  31812  disjxpin  31819  isoun  31923  archirng  32334  archiexdiv  32336  slmdlema  32348  inelcarsg  33310  sibfof  33339  breprexplema  33642  axtgupdim2ALTV  33680  pconncn  34215  ivthALT  35220  poimirlem32  36520  ismtycnv  36670  ismtyima  36671  ismtyres  36676  bfplem1  36690  bfplem2  36691  ghomlinOLD  36756  rngohomadd  36837  rngohommul  36838  crngocom  36869  idladdcl  36887  idllmulcl  36888  idlrmulcl  36889  pridl  36905  ispridlc  36938  pridlc  36939  dmnnzd  36943  oposlem  38052  omllaw  38113  hlsuprexch  38252  lautle  38955  ltrnu  38992  tendovalco  39636  sticksstones1  40962  sticksstones2  40963  ntrkbimka  42789  mullimc  44332  mullimcf  44339  lptre2pt  44356  fourierdlem54  44876  fcoresf1  45779  faovcl  45908  icceuelpartlem  46103  iccpartnel  46106  fargshiftf1  46109  sprsymrelfolem2  46161  reuopreuprim  46194  mgmhmlin  46556  issubmgm2  46560  issubrng2  46737  rnglidlmcl  46748  isthincd2lem2  47656