Theorem rspc2va 3613

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.)

Hypotheses

Ref	Expression
rspc2v.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
rspc2v.2	⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))

Assertion

Ref	Expression
rspc2va	⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝐷,𝑦   𝜒,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑦)   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem rspc2va

Step	Hyp	Ref	Expression
1		rspc2v.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		rspc2v.2	. . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
3	1, 2	rspc2v 3612	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))
4	3	imp 406	1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052

This theorem is referenced by:  rspc2dv  3616  swopo  5572  f1ounsn  7264  soisores  7319  soisoi  7320  isocnv  7322  isotr  7328  ovrspc2v  7429  coof  7693  caofrss  7708  caonncan  7713  frpoins3xpg  8137  coflton  8681  wunpr  10721  injresinj  13802  seqcaopr2  14054  rlimcn3  15604  o1of2  15627  isprm6  16731  ssc2  17833  pospropd  18335  tleile  18429  mgmhmpropd  18674  mhmpropd  18768  grpidssd  18997  grpinvssd  18998  dfgrp3lem  19019  isnsg3  19141  cyccom  19184  symgextf1  19400  efgredlemd  19723  efgredlem  19726  rglcom4d  20169  rnghmmul  20407  domneq0  20666  issrngd  20813  lindfind  21774  lindsind  21775  mplsubglem  21957  mdetunilem1  22548  mdetunilem3  22550  mdetunilem4  22551  mdetunilem9  22556  decpmatmulsumfsupp  22709  pm2mpf1  22735  pm2mpmhmlem1  22754  t0sep  23260  tsmsxplem2  24090  comet  24450  nrmmetd  24511  tngngp  24591  reconnlem2  24765  iscmet3lem1  25241  iscmet3lem2  25242  dchrisumlem1  27450  pntpbnd1  27547  ssltsepc  27755  tgjustc1  28400  tgjustc2  28401  iscgrglt  28439  motcgr  28461  perpneq  28639  foot  28647  f1otrg  28796  axcontlem10  28898  frgr2wwlk1  30256  orngmul  33271  lindsunlem  33610  mndpluscn  33903  unelros  34148  difelros  34149  inelsros  34155  diffiunisros  34156  elmrsubrn  35488  ghomco  37861  sticksstones10  42114  sticksstones12a  42116  fsuppind  42560  mzpcl34  42701  ntrk0kbimka  44010  isotone1  44019  isotone2  44020  nnfoctbdjlem  46432  2arymaptf1  48581