| 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 4696 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) |
| 6 | 1, 2, 5 | mp2an 692 | 1 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ∀wral 3061 Vcvv 3480 {cpr 4628 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-v 3482 df-un 3956 df-sn 4627 df-pr 4629 |
| This theorem is referenced by: fprb 7214 fzprval 13625 fvinim0ffz 13825 wwlktovf1 14996 xpsfrnel 17607 xpsle 17624 isdrs2 18352 pmtrsn 19537 iblcnlem1 25823 lfuhgr1v0e 29271 nbgr2vtx1edg 29367 nbuhgr2vtx1edgb 29369 umgr2v2evd2 29545 2wlklem 29685 dfpth2 29749 2wlkdlem5 29949 2wlkdlem10 29955 clwwlknonex2lem2 30127 3pthdlem1 30183 upgr4cycl4dv4e 30204 subfacp1lem3 35187 poimirlem1 37628 paireqne 47498 requad2 47610 ldepsnlinc 48425 rrx2pnecoorneor 48636 rrx2line 48661 rrx2linest 48663 |
| Copyright terms: Public domain | W3C validator |