![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > r19.28zv | Structured version Visualization version GIF version |
Description: Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 19-Aug-2004.) |
Ref | Expression |
---|---|
r19.28zv | ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1912 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | r19.28z 4504 | 1 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ≠ wne 2938 ∀wral 3059 ∅c0 4339 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-9 2116 ax-12 2175 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-clab 2713 df-cleq 2727 df-ne 2939 df-ral 3060 df-dif 3966 df-nul 4340 |
This theorem is referenced by: raaanv 4524 raltpd 4786 iinrab 5074 iindif2 5082 iinin2 5083 reusv2lem5 5408 xpiindi 5849 dfpo2 6318 fint 6788 ixpiin 8963 neips 23137 txflf 24030 isclmp 25144 diaglbN 41038 dihglbcpreN 41283 2reuimp 47065 |
Copyright terms: Public domain | W3C validator |