Theorem r19.21v 3161

Description: Restricted quantifier version of 19.21v 1940. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (Proof shortened by Wolf Lammen, 11-Dec-2024.)

Assertion

Ref	Expression
r19.21v	⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.21v

Step	Hyp	Ref	Expression
1		pm2.27 42	. . . 4 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
2	1	ralimdv 3150	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 32	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 123	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3132	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3073	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
8	5, 7	ja 186	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
9	3, 8	impbii 209	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3052

This theorem is referenced by:  r19.23v  3163  r19.32v  3169  cbvraldva  3216  rmo4  3688  2reu5lem3  3715  ra4v  3835  rmo3  3839  dftr5  5209  reusv3  5350  tfinds2  7806  tfinds3  7807  fpr3g  8227  wfr3g  8261  tfrlem1  8307  tfr3  8330  oeordi  8515  naddssim  8613  ordiso2  9420  ordtypelem7  9429  cantnf  9602  dfac12lem3  10056  ttukeylem5  10423  ttukeylem6  10424  fpwwe2lem7  10548  grudomon  10728  raluz2  12810  bpolycl  15975  ndvdssub  16336  gcdcllem1  16426  acsfn2  17586  pgpfac1  20011  pgpfac  20015  isdomn5  20643  isdomn2OLD  20645  islindf4  21793  isclo2  23032  1stccn  23407  kgencn  23500  txflf  23950  fclsopn  23958  conway  27775  nn0min  32901  bnj580  35069  bnj852  35077  rdgprc  35986  filnetlem4  36575  poimirlem29  37850  heicant  37856  indstrd  42447  ntrneixb  44336  trfr  45203  modelac8prim  45233  2rexrsb  47348  tfis2d  49925