Theorem rspc2va 3593

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080

This theorem is referenced by:  rspc2dv  3596  swopo  5580  f1ounsn  7270  soisores  7325  soisoi  7326  isocnv  7328  isotr  7334  ovrspc2v  7436  coof  7698  caofrss  7713  caonncan  7718  frpoins3xpg  8132  coflton  8653  wunpr  10689  injresinj  13816  seqcaopr2  14070  rlimcn3  15637  o1of2  15660  isprm6  16768  ssc2  17874  pospropd  18376  tleile  18470  mgmhmpropd  18751  mhmpropd  18845  grpidssd  19077  grpinvssd  19078  dfgrp3lem  19099  isnsg3  19221  cyccom  19269  symgextf1  19486  efgredlemd  19809  efgredlem  19812  rglcom4d  20288  rnghmmul  20527  domneq0  20807  issrngd  20958  orngmul  20968  lindfind  21966  lindsind  21967  mplsubglem  22148  mdetunilem1  22769  mdetunilem3  22771  mdetunilem4  22772  mdetunilem9  22777  decpmatmulsumfsupp  22930  pm2mpf1  22956  pm2mpmhmlem1  22975  t0sep  23481  tsmsxplem2  24311  comet  24670  nrmmetd  24731  tngngp  24811  reconnlem2  24985  iscmet3lem1  25450  iscmet3lem2  25451  dchrisumlem1  27653  pntpbnd1  27750  sltssepc  27964  tgjustc1  28744  tgjustc2  28745  iscgrglt  28783  motcgr  28805  perpneq  28994  foot  29002  f1otrg  29220  axcontlem10  29323  frgr2wwlk1  30680  lindsunlem  34014  mndpluscn  34316  unelros  34561  difelros  34562  inelsros  34568  diffiunisros  34569  elmrsubrn  36012  nmuladdel  36704  ghomco  38562  sticksstones10  42942  sticksstones12a  42944  fsuppind  43342  mzpcl34  43482  ntrk0kbimka  44785  isotone1  44794  isotone2  44795  nnfoctbdjlem  47189  2arymaptf1  49453