![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralpr | Structured version Visualization version GIF version |
Description: Convert a restricted universal quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.) |
Ref | Expression |
---|---|
ralpr.1 | ⊢ 𝐴 ∈ V |
ralpr.2 | ⊢ 𝐵 ∈ V |
ralpr.3 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
ralpr.4 | ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralpr | ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralpr.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | ralpr.2 | . 2 ⊢ 𝐵 ∈ V | |
3 | ralpr.3 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | ralpr.4 | . . 3 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) | |
5 | 3, 4 | ralprg 4699 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) |
6 | 1, 2, 5 | mp2an 691 | 1 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∀wral 3062 Vcvv 3475 {cpr 4631 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-v 3477 df-un 3954 df-sn 4630 df-pr 4632 |
This theorem is referenced by: fprb 7195 fzprval 13562 fvinim0ffz 13751 wwlktovf1 14908 xpsfrnel 17508 xpsle 17525 isdrs2 18259 pmtrsn 19387 iblcnlem1 25305 lfuhgr1v0e 28511 nbgr2vtx1edg 28607 nbuhgr2vtx1edgb 28609 umgr2v2evd2 28784 2wlklem 28924 2wlkdlem5 29183 2wlkdlem10 29189 clwwlknonex2lem2 29361 3pthdlem1 29417 upgr4cycl4dv4e 29438 subfacp1lem3 34173 poimirlem1 36489 paireqne 46179 requad2 46291 ldepsnlinc 47189 rrx2pnecoorneor 47401 rrx2line 47426 rrx2linest 47428 |
Copyright terms: Public domain | W3C validator |