Theorem rspc2va 3582

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-ral 3111

This theorem is referenced by:  swopo  5448  soisores  7059  soisoi  7060  isocnv  7062  isotr  7068  ovrspc2v  7161  caofrss  7422  caonncan  7427  wunpr  10120  injresinj  13153  seqcaopr2  13402  rlimcn2  14939  o1of2  14961  isprm6  16048  ssc2  17084  pospropd  17736  mhmpropd  17954  grpidssd  18167  grpinvssd  18168  dfgrp3lem  18189  isnsg3  18304  cyccom  18338  symgextf1  18541  efgredlemd  18862  efgredlem  18865  issrngd  19625  domneq0  20063  lindfind  20505  lindsind  20506  mplsubglem  20672  mdetunilem1  21217  mdetunilem3  21219  mdetunilem4  21220  mdetunilem9  21225  decpmatmulsumfsupp  21378  pm2mpf1  21404  pm2mpmhmlem1  21423  t0sep  21929  tsmsxplem2  22759  comet  23120  nrmmetd  23181  tngngp  23260  reconnlem2  23432  iscmet3lem1  23895  iscmet3lem2  23896  dchrisumlem1  26073  pntpbnd1  26170  tgjustc1  26269  tgjustc2  26270  iscgrglt  26308  motcgr  26330  perpneq  26508  foot  26516  f1otrg  26665  axcontlem10  26767  frgr2wwlk1  28114  tleile  30674  orngmul  30927  lindsunlem  31108  mndpluscn  31279  unelros  31540  difelros  31541  inelsros  31547  diffiunisros  31548  cvxsconn  32603  elmrsubrn  32880  ghomco  35329  fsuppind  39456  mzpcl34  39672  ntrk0kbimka  40742  isotone1  40751  isotone2  40752  nnfoctbdjlem  43094  isomuspgrlem2d  44349  mgmhmpropd  44405  rnghmmul  44524  2arymaptf1  45067