Theorem r19.21v 3177

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  r19.23v  3180  r19.32v  3189  cbvraldva  3236  rmo4  3738  2reu5lem3  3765  ra4v  3893  rmo3  3897  dftr5  5268  dftr5OLD  5269  reusv3  5410  tfinds2  7884  tfinds3  7885  fpr3g  8308  wfr3g  8345  tfrlem1  8414  tfr3  8437  oeordi  8623  naddssim  8721  ordiso2  9552  ordtypelem7  9561  cantnf  9730  dfac12lem3  10183  ttukeylem5  10550  ttukeylem6  10551  fpwwe2lem7  10674  grudomon  10854  raluz2  12936  bpolycl  16084  ndvdssub  16442  gcdcllem1  16532  acsfn2  17707  pgpfac1  20114  pgpfac  20118  isdomn5  20726  isdomn2OLD  20728  islindf4  21875  isclo2  23111  1stccn  23486  kgencn  23579  txflf  24029  fclsopn  24037  conway  27858  nn0min  32826  bnj580  34905  bnj852  34913  rdgprc  35775  filnetlem4  36363  poimirlem29  37635  heicant  37641  indstrd  42174  ntrneixb  44084  2rexrsb  47051  tfis2d  48910