Theorem rspc2va 3602

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086

This theorem is referenced by:  rspc2dv  3605  swopo  5581  f1ounsn  7271  soisores  7326  soisoi  7327  isocnv  7329  isotr  7335  ovrspc2v  7437  coof  7699  caofrss  7714  caonncan  7719  frpoins3xpg  8136  coflton  8657  wunpr  10694  injresinj  13820  seqcaopr2  14074  rlimcn3  15641  o1of2  15664  isprm6  16773  ssc2  17879  pospropd  18381  tleile  18475  mgmhmpropd  18756  mhmpropd  18850  grpidssd  19082  grpinvssd  19083  dfgrp3lem  19104  isnsg3  19226  cyccom  19274  symgextf1  19491  efgredlemd  19814  efgredlem  19817  rglcom4d  20293  rnghmmul  20531  domneq0  20793  issrngd  20936  orngmul  20946  lindfind  21935  lindsind  21936  mplsubglem  22117  mdetunilem1  22738  mdetunilem3  22740  mdetunilem4  22741  mdetunilem9  22746  decpmatmulsumfsupp  22899  pm2mpf1  22925  pm2mpmhmlem1  22944  t0sep  23450  tsmsxplem2  24280  comet  24639  nrmmetd  24700  tngngp  24780  reconnlem2  24954  iscmet3lem1  25419  iscmet3lem2  25420  dchrisumlem1  27619  pntpbnd1  27716  sltssepc  27930  tgjustc1  28710  tgjustc2  28711  iscgrglt  28749  motcgr  28771  perpneq  28953  foot  28961  f1otrg  29161  axcontlem10  29264  frgr2wwlk1  30621  lindsunlem  33959  mndpluscn  34261  unelros  34506  difelros  34507  inelsros  34513  diffiunisros  34514  elmrsubrn  35945  ghomco  38464  sticksstones10  42846  sticksstones12a  42848  fsuppind  43248  mzpcl34  43388  ntrk0kbimka  44691  isotone1  44700  isotone2  44701  nnfoctbdjlem  47095  2arymaptf1  49352