Theorem r19.21v 3179

Description: Restricted quantifier version of 19.21v 1942. (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 3169	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 32	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 123	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3150	. . 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 3061

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3062

This theorem is referenced by:  r19.23v  3182  r19.32v  3191  cbvraldva  3236  rmo4  3726  2reu5lem3  3753  ra4v  3879  rmo3  3883  dftr5  5269  dftr5OLD  5270  reusv3  5403  tfinds2  7855  tfinds3  7856  fpr3g  8272  wfr3g  8309  tfrlem1  8378  tfr3  8401  oeordi  8589  naddssim  8686  ordiso2  9512  ordtypelem7  9521  cantnf  9690  dfac12lem3  10142  ttukeylem5  10510  ttukeylem6  10511  fpwwe2lem7  10634  grudomon  10814  raluz2  12885  bpolycl  16000  ndvdssub  16356  gcdcllem1  16444  acsfn2  17611  pgpfac1  19991  pgpfac  19995  isdomn2  21115  isdomn5  21117  islindf4  21612  isclo2  22812  1stccn  23187  kgencn  23280  txflf  23730  fclsopn  23738  conway  27525  nn0min  32281  bnj580  34210  bnj852  34218  rdgprc  35058  filnetlem4  35569  poimirlem29  36820  heicant  36826  ntrneixb  43148  2rexrsb  46109  tfis2d  47813