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 397	1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1656   ∈ wcel 2164  ∀wral 3117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-v 3416

This theorem is referenced by:  swopo  5275  soisores  6837  soisoi  6838  isocnv  6840  isotr  6846  ovrspc2v  6936  off  7177  caofrss  7195  caonncan  7200  wunpr  9853  injresinj  12891  seqcaopr2  13138  rlimcn2  14705  o1of2  14727  isprm6  15804  ssc2  16841  pospropd  17494  mhmpropd  17701  grpidssd  17852  grpinvssd  17853  dfgrp3lem  17874  isnsg3  17986  symgextf1  18198  efgredlemd  18516  efgredlem  18519  efgredlemOLD  18520  issrngd  19224  domneq0  19665  mplsubglem  19802  lindfind  20529  lindsind  20530  mdetunilem1  20793  mdetunilem3  20795  mdetunilem4  20796  mdetunilem9  20801  decpmatmulsumfsupp  20955  pm2mpf1  20981  pm2mpmhmlem1  21000  t0sep  21506  tsmsxplem2  22334  comet  22695  nrmmetd  22756  tngngp  22835  reconnlem2  23007  iscmet3lem1  23466  iscmet3lem2  23467  dchrisumlem1  25598  pntpbnd1  25695  tgjustc1  25794  tgjustc2  25795  motcgr  25855  perpneq  26033  foot  26038  f1otrg  26177  axcontlem10  26279  frgr2wwlk1  27706  tleile  30202  orngmul  30344  mndpluscn  30513  unelros  30775  difelros  30776  inelsros  30782  diffiunisros  30783  cvxsconn  31767  elmrsubrn  31959  ghomco  34227  mzpcl34  38133  ntrk0kbimka  39172  isotone1  39181  isotone2  39182  nnfoctbdjlem  41457  isomuspgrlem2d  42563  mgmhmpropd  42646  rnghmmul  42761