Theorem r19.21v 3163

Description: Restricted quantifier version of 19.21v 1941. (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 3152	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 32	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 123	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3134	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3075	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
8	5, 7	ja 186	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
9	3, 8	impbii 209	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

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

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 1912

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

This theorem is referenced by:  r19.23v  3165  r19.32v  3171  cbvraldva  3218  rmo4  3690  2reu5lem3  3717  ra4v  3837  rmo3  3841  dftr5  5211  reusv3  5352  tfinds2  7816  tfinds3  7817  fpr3g  8237  wfr3g  8271  tfrlem1  8317  tfr3  8340  oeordi  8525  naddssim  8623  ordiso2  9432  ordtypelem7  9441  cantnf  9614  dfac12lem3  10068  ttukeylem5  10435  ttukeylem6  10436  fpwwe2lem7  10560  grudomon  10740  raluz2  12822  bpolycl  15987  ndvdssub  16348  gcdcllem1  16438  acsfn2  17598  pgpfac1  20023  pgpfac  20027  isdomn5  20655  isdomn2OLD  20657  islindf4  21805  isclo2  23044  1stccn  23419  kgencn  23512  txflf  23962  fclsopn  23970  conway  27787  nn0min  32912  bnj580  35089  bnj852  35097  rdgprc  36008  filnetlem4  36597  poimirlem29  37900  heicant  37906  indstrd  42563  ntrneixb  44451  trfr  45318  modelac8prim  45348  2rexrsb  47462  tfis2d  50039