Theorem rspc2va 3323

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202

This theorem is referenced by:  swopo  5045  soisores  6577  soisoi  6578  isocnv  6580  isotr  6586  ovrspc2v  6672  off  6912  caofrss  6930  caonncan  6935  wunpr  9531  injresinj  12589  seqcaopr2  12837  rlimcn2  14321  o1of2  14343  isprm6  15426  ssc2  16482  pospropd  17134  mhmpropd  17341  grpidssd  17491  grpinvssd  17492  dfgrp3lem  17513  isnsg3  17628  symgextf1  17841  efgredlemd  18157  efgredlem  18160  issrngd  18861  domneq0  19297  mplsubglem  19434  lindfind  20155  lindsind  20156  mdetunilem1  20418  mdetunilem3  20420  mdetunilem4  20421  mdetunilem9  20426  decpmatmulsumfsupp  20578  pm2mpf1  20604  pm2mpmhmlem1  20623  t0sep  21128  tsmsxplem2  21957  comet  22318  nrmmetd  22379  tngngp  22458  reconnlem2  22630  iscmet3lem1  23089  iscmet3lem2  23090  dchrisumlem1  25178  pntpbnd1  25275  motcgr  25431  perpneq  25609  foot  25614  f1otrg  25751  axcontlem10  25853  frgr2wwlk1  27193  tleile  29661  orngmul  29803  mndpluscn  29972  unelros  30234  difelros  30235  inelsros  30241  diffiunisros  30242  cvxsconn  31225  elmrsubrn  31417  ghomco  33690  mzpcl34  37294  ntrk0kbimka  38337  isotone1  38346  isotone2  38347  nnfoctbdjlem  40672  mgmhmpropd  41785  rnghmmul  41900