Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > r19.26-2 | Structured version Visualization version GIF version |
Description: Restricted quantifier version of 19.26-2 1787. Version of r19.26 3046 with two quantifiers. (Contributed by NM, 10-Aug-2004.) |
Ref | Expression |
---|---|
r19.26-2 | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.26 3046 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)) | |
2 | 1 | ralbii 2963 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)) |
3 | r19.26 3046 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) | |
4 | 2, 3 | bitri 263 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ral 2901 |
This theorem is referenced by: fununi 5878 tz7.48lem 7423 isffth2 16399 ispos2 16771 issgrpv 17109 issgrpn0 17110 isnsg2 17447 efgred 17984 dfrhm2 18540 cpmatacl 20340 cpmatmcllem 20342 caucfil 22889 aalioulem6 23896 ajmoi 27098 adjmo 28075 iccllyscon 30486 dfso3 30856 ispridl2 33007 ishlat2 33658 fiinfi 36897 ntrk1k3eqk13 37368 isrnghm 41682 |
Copyright terms: Public domain | W3C validator |