Theorem rspc2va 3571

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069

This theorem is referenced by:  swopo  5514  soisores  7198  soisoi  7199  isocnv  7201  isotr  7207  ovrspc2v  7301  caofrss  7569  caonncan  7574  wunpr  10465  injresinj  13508  seqcaopr2  13759  rlimcn3  15299  o1of2  15322  isprm6  16419  ssc2  17534  pospropd  18045  tleile  18139  mhmpropd  18436  grpidssd  18651  grpinvssd  18652  dfgrp3lem  18673  isnsg3  18788  cyccom  18822  symgextf1  19029  efgredlemd  19350  efgredlem  19353  issrngd  20121  domneq0  20568  lindfind  21023  lindsind  21024  mplsubglem  21205  mdetunilem1  21761  mdetunilem3  21763  mdetunilem4  21764  mdetunilem9  21769  decpmatmulsumfsupp  21922  pm2mpf1  21948  pm2mpmhmlem1  21967  t0sep  22475  tsmsxplem2  23305  comet  23669  nrmmetd  23730  tngngp  23818  reconnlem2  23990  iscmet3lem1  24455  iscmet3lem2  24456  dchrisumlem1  26637  pntpbnd1  26734  tgjustc1  26836  tgjustc2  26837  iscgrglt  26875  motcgr  26897  perpneq  27075  foot  27083  f1otrg  27232  axcontlem10  27341  frgr2wwlk1  28693  orngmul  31502  lindsunlem  31705  mndpluscn  31876  unelros  32139  difelros  32140  inelsros  32146  diffiunisros  32147  cvxsconn  33205  elmrsubrn  33482  frpoins3xpg  33787  ssltsepc  33987  ghomco  36049  sticksstones10  40111  sticksstones12a  40113  fsuppind  40279  mzpcl34  40553  ntrk0kbimka  41649  isotone1  41658  isotone2  41659  nnfoctbdjlem  43993  isomuspgrlem2d  45283  mgmhmpropd  45339  rnghmmul  45458  2arymaptf1  45999