![]() |
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 1950. Version of r19.26 3212 with two quantifiers. (Contributed by NM, 10-Aug-2004.) |
Ref | Expression |
---|---|
r19.26-2 | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.26 3212 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)) | |
2 | 1 | ralbii 3129 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)) |
3 | r19.26 3212 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) | |
4 | 2, 3 | bitri 264 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 382 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ral 3066 |
This theorem is referenced by: fununi 6104 tz7.48lem 7689 isffth2 16783 ispos2 17156 issgrpv 17494 issgrpn0 17495 isnsg2 17832 efgred 18368 dfrhm2 18927 cpmatacl 20741 cpmatmcllem 20743 caucfil 23300 aalioulem6 24312 ajmoi 28054 adjmo 29031 iccllysconn 31570 dfso3 31939 ispridl2 34169 ishlat2 35162 fiinfi 38404 ntrk1k3eqk13 38874 isrnghm 42420 |
Copyright terms: Public domain | W3C validator |