Theorem rspc2va 3540

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542   ∈ wcel 2114  ∀wral 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ral 3059

This theorem is referenced by:  swopo  5463  soisores  7106  soisoi  7107  isocnv  7109  isotr  7115  ovrspc2v  7209  caofrss  7473  caonncan  7478  wunpr  10222  injresinj  13262  seqcaopr2  13511  rlimcn3  15050  o1of2  15073  isprm6  16168  ssc2  17210  pospropd  17873  mhmpropd  18091  grpidssd  18306  grpinvssd  18307  dfgrp3lem  18328  isnsg3  18443  cyccom  18477  symgextf1  18680  efgredlemd  19001  efgredlem  19004  issrngd  19764  domneq0  20202  lindfind  20645  lindsind  20646  mplsubglem  20828  mdetunilem1  21376  mdetunilem3  21378  mdetunilem4  21379  mdetunilem9  21384  decpmatmulsumfsupp  21537  pm2mpf1  21563  pm2mpmhmlem1  21582  t0sep  22088  tsmsxplem2  22918  comet  23279  nrmmetd  23340  tngngp  23420  reconnlem2  23592  iscmet3lem1  24056  iscmet3lem2  24057  dchrisumlem1  26238  pntpbnd1  26335  tgjustc1  26434  tgjustc2  26435  iscgrglt  26473  motcgr  26495  perpneq  26673  foot  26681  f1otrg  26830  axcontlem10  26932  frgr2wwlk1  28279  tleile  30834  orngmul  31092  lindsunlem  31290  mndpluscn  31461  unelros  31722  difelros  31723  inelsros  31729  diffiunisros  31730  cvxsconn  32789  elmrsubrn  33066  frpoins3xpg  33403  ssltsepc  33643  ghomco  35705  sticksstones10  39750  sticksstones12a  39752  fsuppind  39899  mzpcl34  40166  ntrk0kbimka  41236  isotone1  41245  isotone2  41246  nnfoctbdjlem  43576  isomuspgrlem2d  44865  mgmhmpropd  44921  rnghmmul  45040  2arymaptf1  45581