Theorem rspc2va 3623

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 3622	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))
4	3	imp 407	1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062

This theorem is referenced by:  rspc2dv  3626  swopo  5599  soisores  7323  soisoi  7324  isocnv  7326  isotr  7332  ovrspc2v  7434  caofrss  7705  caonncan  7710  frpoins3xpg  8125  coflton  8669  wunpr  10703  injresinj  13752  seqcaopr2  14003  rlimcn3  15533  o1of2  15556  isprm6  16650  ssc2  17768  pospropd  18279  tleile  18373  mhmpropd  18677  grpidssd  18898  grpinvssd  18899  dfgrp3lem  18920  isnsg3  19039  cyccom  19079  symgextf1  19288  efgredlemd  19611  efgredlem  19614  rglcom4d  20033  issrngd  20468  domneq0  20912  lindfind  21370  lindsind  21371  mplsubglem  21557  mdetunilem1  22113  mdetunilem3  22115  mdetunilem4  22116  mdetunilem9  22121  decpmatmulsumfsupp  22274  pm2mpf1  22300  pm2mpmhmlem1  22319  t0sep  22827  tsmsxplem2  23657  comet  24021  nrmmetd  24082  tngngp  24170  reconnlem2  24342  iscmet3lem1  24807  iscmet3lem2  24808  dchrisumlem1  26989  pntpbnd1  27086  ssltsepc  27291  tgjustc1  27723  tgjustc2  27724  iscgrglt  27762  motcgr  27784  perpneq  27962  foot  27970  f1otrg  28119  axcontlem10  28228  frgr2wwlk1  29579  orngmul  32416  lindsunlem  32704  mndpluscn  32901  unelros  33164  difelros  33165  inelsros  33171  diffiunisros  33172  cvxsconn  34229  elmrsubrn  34506  ghomco  36754  sticksstones10  40966  sticksstones12a  40968  fsuppind  41164  mzpcl34  41459  ntrk0kbimka  42780  isotone1  42789  isotone2  42790  nnfoctbdjlem  45161  isomuspgrlem2d  46489  mgmhmpropd  46545  rnghmmul  46688  2arymaptf1  47329