![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > riota2 | GIF version |
Description: This theorem shows a condition that allows us to represent a descriptor with a class expression 𝐵. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.) |
Ref | Expression |
---|---|
riota2.1 | ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
riota2 | ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2319 | . 2 ⊢ Ⅎ𝑥𝐵 | |
2 | nfv 1528 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | riota2.1 | . 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | riota2f 5845 | 1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1353 ∈ wcel 2148 ∃!wreu 2457 ℩crio 5823 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-eu 2029 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-rex 2461 df-reu 2462 df-v 2739 df-sbc 2963 df-un 3133 df-sn 3597 df-pr 3598 df-uni 3808 df-iota 5173 df-riota 5824 |
This theorem is referenced by: eqsupti 6988 prsrriota 7765 recriota 7867 axcaucvglemval 7874 subadd 8137 divmulap 8608 flqlelt 10249 flqbi 10263 remim 10840 resqrtcl 11009 rersqrtthlem 11010 divalgmod 11902 dfgcd3 11981 bezout 11982 oddpwdclemxy 12139 qnumdenbi 12162 ismgmid 12675 isgrpinv 12803 |
Copyright terms: Public domain | W3C validator |