![]() |
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 4543 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) |
6 | 1, 2, 5 | mp2an 688 | 1 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1522 ∈ wcel 2081 ∀wral 3105 Vcvv 3437 {cpr 4478 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-v 3439 df-sbc 3710 df-un 3868 df-sn 4477 df-pr 4479 |
This theorem is referenced by: fprb 6828 fzprval 12823 fvinim0ffz 13011 wwlktovf1 14160 xpsfrnel 16669 xpsle 16686 isdrs2 17383 pmtrsn 18383 iblcnlem1 24076 lfuhgr1v0e 26724 nbgr2vtx1edg 26820 nbuhgr2vtx1edgb 26822 umgr2v2evd2 26997 2wlklem 27136 2wlkdlem5 27400 2wlkdlem10 27406 clwwlknonex2lem2 27579 3pthdlem1 27635 upgr4cycl4dv4e 27656 subfacp1lem3 32043 poimirlem1 34449 paireqne 43181 requad2 43296 ldepsnlinc 44069 rrx2pnecoorneor 44209 rrx2line 44234 rrx2linest 44236 |
Copyright terms: Public domain | W3C validator |