Theorem r19.21v 3165

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 3154	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 32	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 123	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3136	. . 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 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  r19.23v  3168  r19.32v  3177  cbvraldva  3222  rmo4  3713  2reu5lem3  3740  ra4v  3860  rmo3  3864  dftr5  5233  dftr5OLD  5234  reusv3  5375  tfinds2  7859  tfinds3  7860  fpr3g  8284  wfr3g  8321  tfrlem1  8390  tfr3  8413  oeordi  8599  naddssim  8697  ordiso2  9529  ordtypelem7  9538  cantnf  9707  dfac12lem3  10160  ttukeylem5  10527  ttukeylem6  10528  fpwwe2lem7  10651  grudomon  10831  raluz2  12913  bpolycl  16068  ndvdssub  16428  gcdcllem1  16518  acsfn2  17675  pgpfac1  20063  pgpfac  20067  isdomn5  20670  isdomn2OLD  20672  islindf4  21798  isclo2  23026  1stccn  23401  kgencn  23494  txflf  23944  fclsopn  23952  conway  27763  nn0min  32799  bnj580  34944  bnj852  34952  rdgprc  35812  filnetlem4  36399  poimirlem29  37673  heicant  37679  indstrd  42206  ntrneixb  44119  trfr  44987  modelac8prim  45017  2rexrsb  47131  tfis2d  49544