| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > r19.21v | Structured version Visualization version GIF version | ||
| 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.) |
| Ref | Expression |
|---|---|
| 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 209 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∀wral 3061 |
| 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 3062 |
| This theorem is referenced by: r19.23v 3183 r19.32v 3192 cbvraldva 3239 rmo4 3736 2reu5lem3 3763 ra4v 3885 rmo3 3889 dftr5 5263 dftr5OLD 5264 reusv3 5405 tfinds2 7885 tfinds3 7886 fpr3g 8310 wfr3g 8347 tfrlem1 8416 tfr3 8439 oeordi 8625 naddssim 8723 ordiso2 9555 ordtypelem7 9564 cantnf 9733 dfac12lem3 10186 ttukeylem5 10553 ttukeylem6 10554 fpwwe2lem7 10677 grudomon 10857 raluz2 12939 bpolycl 16088 ndvdssub 16446 gcdcllem1 16536 acsfn2 17706 pgpfac1 20100 pgpfac 20104 isdomn5 20710 isdomn2OLD 20712 islindf4 21858 isclo2 23096 1stccn 23471 kgencn 23564 txflf 24014 fclsopn 24022 conway 27844 nn0min 32822 bnj580 34927 bnj852 34935 rdgprc 35795 filnetlem4 36382 poimirlem29 37656 heicant 37662 indstrd 42194 ntrneixb 44108 trfr 44979 modelac8prim 45009 2rexrsb 47114 tfis2d 49199 |
| Copyright terms: Public domain | W3C validator |