![]() |
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 1908. (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 375 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))) | |
2 | 1 | albii 1787 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ ∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓))) |
3 | 19.21v 1908 | . . 3 ⊢ (∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) | |
4 | 2, 3 | bitri 264 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) |
5 | df-ral 2946 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓))) | |
6 | df-ral 2946 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
7 | 6 | imbi2i 325 | . 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))) |
8 | 4, 5, 7 | 3bitr4i 292 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∀wal 1521 ∈ wcel 2030 ∀wral 2941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 |
This theorem depends on definitions: df-bi 197 df-ex 1745 df-ral 2946 |
This theorem is referenced by: r19.23v 3052 r19.32v 3112 rmo4 3432 2reu5lem3 3448 ra4v 3557 rmo3 3561 dftr5 4788 reusv3 4906 tfinds2 7105 tfinds3 7106 wfr3g 7458 tfrlem1 7517 tfr3 7540 oeordi 7712 ordiso2 8461 ordtypelem7 8470 cantnf 8628 dfac12lem3 9005 ttukeylem5 9373 ttukeylem6 9374 fpwwe2lem8 9497 grudomon 9677 raluz2 11775 bpolycl 14827 ndvdssub 15180 gcdcllem1 15268 acsfn2 16371 pgpfac1 18525 pgpfac 18529 isdomn2 19347 islindf4 20225 isclo2 20940 1stccn 21314 kgencn 21407 txflf 21857 fclsopn 21865 nn0min 29695 bnj580 31109 bnj852 31117 rdgprc 31824 conway 32035 filnetlem4 32501 poimirlem29 33568 heicant 33574 ntrneixb 38710 2rexrsb 41492 tfis2d 42752 |
Copyright terms: Public domain | W3C validator |