|   | 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 1871. Version of r19.26 3111 with two quantifiers. (Contributed by NM, 10-Aug-2004.) | 
| Ref | Expression | 
|---|---|
| r19.26-2 | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | r19.26 3111 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)) | |
| 2 | 1 | ralbii 3093 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)) | 
| 3 | r19.26 3111 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) | |
| 4 | 2, 3 | bitri 275 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 ∀wral 3061 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ral 3062 | 
| This theorem is referenced by: fununi 6641 tz7.48lem 8481 isffth2 17963 ispos2 18361 issgrpv 18734 issgrpn0 18735 isnsg2 19174 efgred 19766 isrnghm 20441 dfrhm2 20474 df2idl2rng 21266 cpmatacl 22722 cpmatmcllem 22724 caucfil 25317 aalioulem6 26379 ajmoi 30877 adjmo 31851 prmidl2 33469 iccllysconn 35255 dfso3 35720 fvineqsnf1 37411 ispridl2 38045 ishlat2 39354 fiinfi 43586 ntrk1k3eqk13 44063 | 
| Copyright terms: Public domain | W3C validator |