![]() |
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 4698 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) |
6 | 1, 2, 5 | mp2an 690 | 1 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3061 Vcvv 3474 {cpr 4630 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ral 3062 df-rex 3071 df-v 3476 df-un 3953 df-sn 4629 df-pr 4631 |
This theorem is referenced by: fprb 7194 fzprval 13561 fvinim0ffz 13750 wwlktovf1 14907 xpsfrnel 17507 xpsle 17524 isdrs2 18258 pmtrsn 19386 iblcnlem1 25304 lfuhgr1v0e 28508 nbgr2vtx1edg 28604 nbuhgr2vtx1edgb 28606 umgr2v2evd2 28781 2wlklem 28921 2wlkdlem5 29180 2wlkdlem10 29186 clwwlknonex2lem2 29358 3pthdlem1 29414 upgr4cycl4dv4e 29435 subfacp1lem3 34168 poimirlem1 36484 paireqne 46169 requad2 46281 ldepsnlinc 47179 rrx2pnecoorneor 47391 rrx2line 47416 rrx2linest 47418 |
Copyright terms: Public domain | W3C validator |