Theorem rspcimdv 3570

Description: Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)

Hypotheses

Ref	Expression
rspcimdv.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
rspcimdv.2	⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))

Assertion

Ref	Expression
rspcimdv	⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥   𝜒,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem rspcimdv

Step	Hyp	Ref	Expression
1		df-ral 3078	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓))
2		rspcimdv.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
3		simpr 489	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝑥 = 𝐴)
4	3	eleq1d 2846	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5	4	biimprd 251	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐵))
6		rspcimdv.2	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))
7	5, 6	imim12d 82	. . . 4 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝑥 ∈ 𝐵 → 𝜓) → (𝐴 ∈ 𝐵 → 𝜒)))
8	2, 7	spcimdv 3551	. . 3 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜓) → (𝐴 ∈ 𝐵 → 𝜒)))
9	2, 8	mpid 45	. 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜓) → 𝜒))
10	1, 9	biimtrid 245	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 400  ∀wal 1566   = wceq 1568   ∈ wcel 2141  ∀wral 3077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078

This theorem is referenced by:  rspcimedv  3571  rspcdv  3572  wrd2ind  14759  mreexd  17697  mreexexlemd  17699  catcocl  17740  catass  17741  moni  17792  subccocl  17901  funcco  17927  fullfo  17970  fthf1  17975  nati  18014  acsfiindd  18608  chpscmat  22978  mpomulcn  25005  friendshipgt3  30715  lmxrge0  34308  funressnfv  47725  cfsetsnfsetf1  47741