Theorem r19.21v 3173

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 3163	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 32	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 123	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3144	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3083	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
8	5, 7	ja 186	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
9	3, 8	impbii 208	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3063

This theorem is referenced by:  r19.23v  3176  r19.32v  3185  rmo4  3670  2reu5lem3  3697  ra4v  3823  rmo3  3827  dftr5  5202  dftr5OLD  5203  reusv3  5337  tfinds2  7742  tfinds3  7743  fpr3g  8132  wfr3g  8169  tfrlem1  8238  tfr3  8261  oeordi  8449  ordiso2  9318  ordtypelem7  9327  cantnf  9495  dfac12lem3  9947  ttukeylem5  10315  ttukeylem6  10316  fpwwe2lem7  10439  grudomon  10619  raluz2  12683  bpolycl  15807  ndvdssub  16163  gcdcllem1  16251  acsfn2  17417  pgpfac1  19728  pgpfac  19732  isdomn2  20615  islindf4  21090  isclo2  22284  1stccn  22659  kgencn  22752  txflf  23202  fclsopn  23210  nn0min  31179  bnj580  32938  bnj852  32946  rdgprc  33815  naddssim  33882  conway  34038  filnetlem4  34615  poimirlem29  35850  heicant  35856  isdomn5  40213  ntrneixb  41743  2rexrsb  44652  tfis2d  46444