Theorem rspc2va 3636

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895  df-ral 3145

This theorem is referenced by:  swopo  5486  soisores  7082  soisoi  7083  isocnv  7085  isotr  7091  ovrspc2v  7184  caofrss  7444  caonncan  7449  wunpr  10133  injresinj  13161  seqcaopr2  13409  rlimcn2  14949  o1of2  14971  isprm6  16060  ssc2  17094  pospropd  17746  mhmpropd  17964  grpidssd  18177  grpinvssd  18178  dfgrp3lem  18199  isnsg3  18314  cyccom  18348  symgextf1  18551  efgredlemd  18872  efgredlem  18875  issrngd  19634  domneq0  20072  mplsubglem  20216  lindfind  20962  lindsind  20963  mdetunilem1  21223  mdetunilem3  21225  mdetunilem4  21226  mdetunilem9  21231  decpmatmulsumfsupp  21383  pm2mpf1  21409  pm2mpmhmlem1  21428  t0sep  21934  tsmsxplem2  22764  comet  23125  nrmmetd  23186  tngngp  23265  reconnlem2  23437  iscmet3lem1  23896  iscmet3lem2  23897  dchrisumlem1  26067  pntpbnd1  26164  tgjustc1  26263  tgjustc2  26264  iscgrglt  26302  motcgr  26324  perpneq  26502  foot  26510  f1otrg  26659  axcontlem10  26761  frgr2wwlk1  28110  tleile  30650  orngmul  30878  lindsunlem  31022  mndpluscn  31171  unelros  31432  difelros  31433  inelsros  31439  diffiunisros  31440  cvxsconn  32492  elmrsubrn  32769  ghomco  35171  mzpcl34  39335  ntrk0kbimka  40396  isotone1  40405  isotone2  40406  nnfoctbdjlem  42744  isomuspgrlem2d  44003  mgmhmpropd  44059  rnghmmul  44178