Theorem r19.21v 3158

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

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

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 1910

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

This theorem is referenced by:  r19.23v  3161  r19.32v  3170  cbvraldva  3217  rmo4  3701  2reu5lem3  3728  ra4v  3848  rmo3  3852  dftr5  5218  dftr5OLD  5219  reusv3  5360  tfinds2  7840  tfinds3  7841  fpr3g  8264  wfr3g  8298  tfrlem1  8344  tfr3  8367  oeordi  8551  naddssim  8649  ordiso2  9468  ordtypelem7  9477  cantnf  9646  dfac12lem3  10099  ttukeylem5  10466  ttukeylem6  10467  fpwwe2lem7  10590  grudomon  10770  raluz2  12856  bpolycl  16018  ndvdssub  16379  gcdcllem1  16469  acsfn2  17624  pgpfac1  20012  pgpfac  20016  isdomn5  20619  isdomn2OLD  20621  islindf4  21747  isclo2  22975  1stccn  23350  kgencn  23443  txflf  23893  fclsopn  23901  conway  27711  nn0min  32745  bnj580  34903  bnj852  34911  rdgprc  35782  filnetlem4  36369  poimirlem29  37643  heicant  37649  indstrd  42181  ntrneixb  44084  trfr  44952  modelac8prim  44982  2rexrsb  47103  tfis2d  49669