![]() |
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 1940. (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.) |
Ref | Expression |
---|---|
r19.21v | ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi2.04 392 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))) | |
2 | 1 | albii 1821 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ ∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓))) |
3 | 19.21v 1940 | . . 3 ⊢ (∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) | |
4 | 2, 3 | bitri 278 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) |
5 | df-ral 3111 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓))) | |
6 | df-ral 3111 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
7 | 6 | imbi2i 339 | . 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) |
8 | 4, 5, 7 | 3bitr4i 306 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1536 ∈ wcel 2111 ∀wral 3106 |
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 1911 |
This theorem depends on definitions: df-bi 210 df-ex 1782 df-ral 3111 |
This theorem is referenced by: r19.23v 3238 r19.32v 3294 rmo4 3669 2reu5lem3 3696 ra4v 3814 rmo3 3818 dftr5 5139 reusv3 5271 tfinds2 7558 tfinds3 7559 wfr3g 7936 tfrlem1 7995 tfr3 8018 oeordi 8196 ordiso2 8963 ordtypelem7 8972 cantnf 9140 dfac12lem3 9556 ttukeylem5 9924 ttukeylem6 9925 fpwwe2lem8 10048 grudomon 10228 raluz2 12285 bpolycl 15398 ndvdssub 15750 gcdcllem1 15838 acsfn2 16926 pgpfac1 19195 pgpfac 19199 isdomn2 20065 islindf4 20527 isclo2 21693 1stccn 22068 kgencn 22161 txflf 22611 fclsopn 22619 nn0min 30562 bnj580 32295 bnj852 32303 rdgprc 33152 fpr3g 33235 conway 33377 filnetlem4 33842 poimirlem29 35086 heicant 35092 ntrneixb 40798 2rexrsb 43657 tfis2d 45210 |
Copyright terms: Public domain | W3C validator |