mmdefinitions - Intuitionistic Logic Explorer

List of Syntax, Axioms (ax-) and Definitions (df-)

Ref	Expression (see link for any distinct variable requirements)
wn 3	wff ¬ 𝜑
wi 4	wff (𝜑 → 𝜓)
ax-1 5	⊢ (𝜑 → (𝜓 → 𝜑))
ax-2 6	⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
ax-mp 7	⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓
wa 102	wff (𝜑 ∧ 𝜓)
wb 103	wff (𝜑 ↔ 𝜓)
ax-ia1 104	⊢ ((𝜑 ∧ 𝜓) → 𝜑)
ax-ia2 105	⊢ ((𝜑 ∧ 𝜓) → 𝜓)
ax-ia3 106	⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
df-bi 115	⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
ax-in1 577	⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑)
ax-in2 578	⊢ (¬ 𝜑 → (𝜑 → 𝜓))
wo 662	wff (𝜑 ∨ 𝜓)
ax-io 663	⊢ (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓)))
wstab 773	wff STAB 𝜑
df-stab 774	⊢ (STAB 𝜑 ↔ (¬ ¬ 𝜑 → 𝜑))
wdc 776	wff DECID 𝜑
df-dc 777	⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
w3o 919	wff (𝜑 ∨ 𝜓 ∨ 𝜒)
w3a 920	wff (𝜑 ∧ 𝜓 ∧ 𝜒)
df-3or 921	⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
df-3an 922	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
wal 1283	wff ∀𝑥𝜑
cv 1284	class 𝑥
wceq 1285	wff 𝐴 = 𝐵
wtru 1286	wff ⊤
df-tru 1288	⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
wfal 1290	wff ⊥
df-fal 1291	⊢ (⊥ ↔ ¬ ⊤)
wxo 1307	wff (𝜑 ⊻ 𝜓)
df-xor 1308	⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)))
ax-5 1377	⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
ax-7 1378	⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
ax-gen 1379	⊢ 𝜑    ⇒   ⊢ ∀𝑥𝜑
wnf 1390	wff Ⅎ𝑥𝜑
df-nf 1391	⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
wex 1422	wff ∃𝑥𝜑
ax-ie1 1423	⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
ax-ie2 1424	⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))
wcel 1434	wff 𝐴 ∈ 𝐵
ax-8 1436	⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
ax-10 1437	⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
ax-11 1438	⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
ax-i12 1439	⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
ax-bndl 1440	⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
ax-4 1441	⊢ (∀𝑥𝜑 → 𝜑)
ax-13 1445	⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
ax-14 1446	⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
ax-17 1460	⊢ (𝜑 → ∀𝑥𝜑)
ax-i9 1464	⊢ ∃𝑥 𝑥 = 𝑦
ax-ial 1468	⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
ax-i5r 1469	⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∀𝑥𝜑 → 𝜓))
ax-10o 1646	⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
wsb 1687	wff [𝑦 / 𝑥]𝜑
df-sb 1688	⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
ax-16 1737	⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
ax-11o 1746	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
weu 1943	wff ∃!𝑥𝜑
wmo 1944	wff ∃*𝑥𝜑
df-eu 1946	⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
df-mo 1947	⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
ax-ext 2065	⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)
cab 2069	class {𝑥 ∣ 𝜑}
df-clab 2070	⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
df-cleq 2076	⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧)    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
df-clel 2079	⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
wnfc 2210	wff Ⅎ𝑥𝐴
df-nfc 2212	⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
wne 2249	wff 𝐴 ≠ 𝐵
df-ne 2250	⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
wnel 2344	wff 𝐴 ∉ 𝐵
df-nel 2345	⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
wral 2353	wff ∀𝑥 ∈ 𝐴 𝜑
wrex 2354	wff ∃𝑥 ∈ 𝐴 𝜑
wreu 2355	wff ∃!𝑥 ∈ 𝐴 𝜑
wrmo 2356	wff ∃*𝑥 ∈ 𝐴 𝜑
crab 2357	class {𝑥 ∈ 𝐴 ∣ 𝜑}
df-ral 2358	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
df-rex 2359	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
df-reu 2360	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
df-rmo 2361	⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
df-rab 2362	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
cvv 2612	class V
df-v 2614	⊢ V = {𝑥 ∣ 𝑥 = 𝑥}
wcdeq 2809	wff CondEq(𝑥 = 𝑦 → 𝜑)
df-cdeq 2810	⊢ (CondEq(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜑))
wsbc 2826	wff [𝐴 / 𝑥]𝜑
df-sbc 2827	⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
csb 2919	class ⦋𝐴 / 𝑥⦌𝐵
df-csb 2920	⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
cdif 2981	class (𝐴 ∖ 𝐵)
cun 2982	class (𝐴 ∪ 𝐵)
cin 2983	class (𝐴 ∩ 𝐵)
wss 2984	wff 𝐴 ⊆ 𝐵
df-dif 2986	⊢ (𝐴 ∖ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)}
df-un 2988	⊢ (𝐴 ∪ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)}
df-in 2990	⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
df-ss 2997	⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
c0 3269	class ∅
df-nul 3270	⊢ ∅ = (V ∖ V)
cif 3373	class if(𝜑, 𝐴, 𝐵)
df-if 3374	⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ ¬ 𝜑))}
cpw 3406	class 𝒫 𝐴
df-pw 3408	⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴}
csn 3422	class {𝐴}
cpr 3423	class {𝐴, 𝐵}
ctp 3424	class {𝐴, 𝐵, 𝐶}
cop 3425	class ⟨𝐴, 𝐵⟩
cotp 3426	class ⟨𝐴, 𝐵, 𝐶⟩
df-sn 3428	⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
df-pr 3429	⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
df-tp 3430	⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
df-op 3431	⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
df-ot 3432	⊢ ⟨𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩
cuni 3627	class ∪ 𝐴
df-uni 3628	⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)}
cint 3662	class ∩ 𝐴
df-int 3663	⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦)}
ciun 3704	class ∪ 𝑥 ∈ 𝐴 𝐵
ciin 3705	class ∩ 𝑥 ∈ 𝐴 𝐵
df-iun 3706	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
df-iin 3707	⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
wdisj 3792	wff Disj 𝑥 ∈ 𝐴 𝐵
df-disj 3793	⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
wbr 3811	wff 𝐴𝑅𝐵
df-br 3812	⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
copab 3864	class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
cmpt 3865	class (𝑥 ∈ 𝐴 ↦ 𝐵)
df-opab 3866	⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
df-mpt 3867	⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
wtr 3901	wff Tr 𝐴
df-tr 3902	⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
ax-coll 3919	⊢ Ⅎ𝑏𝜑    ⇒   ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑)
ax-sep 3922	⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
ax-nul 3930	⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
ax-pow 3974	⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
wem 3993	wff EXMID
df-exmid 3994	⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥))
ax-pr 4000	⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
cep 4078	class E
cid 4079	class I
df-eprel 4080	⊢ E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}
df-id 4084	⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
wpo 4085	wff 𝑅 Po 𝐴
wor 4086	wff 𝑅 Or 𝐴
df-po 4087	⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
df-iso 4088	⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))))
wfrfor 4118	wff FrFor 𝑅𝐴𝑆
wfr 4119	wff 𝑅 Fr 𝐴
wse 4120	wff 𝑅 Se 𝐴
wwe 4121	wff 𝑅 We 𝐴
df-frfor 4122	⊢ ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆))
df-frind 4123	⊢ (𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠)
df-se 4124	⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V)
df-wetr 4125	⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
word 4153	wff Ord 𝐴
con0 4154	class On
wlim 4155	wff Lim 𝐴
csuc 4156	class suc 𝐴
df-iord 4157	⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥))
df-on 4159	⊢ On = {𝑥 ∣ Ord 𝑥}
df-ilim 4160	⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴))
df-suc 4162	⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
ax-un 4224	⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
ax-setind 4316	⊢ (∀𝑎(∀𝑦 ∈ 𝑎 [𝑦 / 𝑎]𝜑 → 𝜑) → ∀𝑎𝜑)
ax-iinf 4366	⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥))
com 4368	class ω
df-iom 4369	⊢ ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}
cxp 4399	class (𝐴 × 𝐵)
ccnv 4400	class ◡𝐴
cdm 4401	class dom 𝐴
crn 4402	class ran 𝐴
cres 4403	class (𝐴 ↾ 𝐵)
cima 4404	class (𝐴 “ 𝐵)
ccom 4405	class (𝐴 ∘ 𝐵)
wrel 4406	wff Rel 𝐴
df-xp 4407	⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
df-rel 4408	⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
df-cnv 4409	⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
df-co 4410	⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}
df-dm 4411	⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
df-rn 4412	⊢ ran 𝐴 = dom ◡𝐴
df-res 4413	⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
df-ima 4414	⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
cio 4932	class (℩𝑥𝜑)
df-iota 4934	⊢ (℩𝑥𝜑) = ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
wfun 4963	wff Fun 𝐴
wfn 4964	wff 𝐴 Fn 𝐵
wf 4965	wff 𝐹:𝐴⟶𝐵
wf1 4966	wff 𝐹:𝐴–1-1→𝐵
wfo 4967	wff 𝐹:𝐴–onto→𝐵
wf1o 4968	wff 𝐹:𝐴–1-1-onto→𝐵
cfv 4969	class (𝐹‘𝐴)
wiso 4970	wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
df-fun 4971	⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
df-fn 4972	⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))
df-f 4973	⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
df-f1 4974	⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
df-fo 4975	⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
df-f1o 4976	⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
df-fv 4977	⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
df-isom 4978	⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
crio 5546	class (℩𝑥 ∈ 𝐴 𝜑)
df-riota 5547	⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
co 5591	class (𝐴𝐹𝐵)
coprab 5592	class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
cmpt2 5593	class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
df-ov 5594	⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
df-oprab 5595	⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
df-mpt2 5596	⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
cof 5789	class ∘𝑓 𝑅
cofr 5790	class ∘𝑟 𝑅
df-of 5791	⊢ ∘𝑓 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓‘𝑥)𝑅(𝑔‘𝑥))))
df-ofr 5792	⊢ ∘𝑟 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)}
c1st 5844	class 1st
c2nd 5845	class 2nd
df-1st 5846	⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
df-2nd 5847	⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥})
ctpos 5941	class tpos 𝐹
df-tpos 5942	⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
wsmo 5982	wff Smo 𝐴
df-smo 5983	⊢ (Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))))
crecs 6001	class recs(𝐹)
df-recs 6002	⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
crdg 6066	class rec(𝐹, 𝐼)
df-irdg 6067	⊢ rec(𝐹, 𝐼) = recs((𝑔 ∈ V ↦ (𝐼 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))))
cfrec 6087	class frec(𝐹, 𝐼)
df-frec 6088	⊢ frec(𝐹, 𝐼) = (recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐼))})) ↾ ω)
c1o 6106	class 1𝑜
c2o 6107	class 2𝑜
c3o 6108	class 3𝑜
c4o 6109	class 4𝑜
coa 6110	class +𝑜
comu 6111	class ·𝑜
coei 6112	class ↑𝑜
df-1o 6113	⊢ 1𝑜 = suc ∅
df-2o 6114	⊢ 2𝑜 = suc 1𝑜
df-3o 6115	⊢ 3𝑜 = suc 2𝑜
df-4o 6116	⊢ 4𝑜 = suc 3𝑜
df-oadd 6117	⊢ +𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦))
df-omul 6118	⊢ ·𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +𝑜 𝑥)), ∅)‘𝑦))
df-oexpi 6119	⊢ ↑𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·𝑜 𝑥)), 1𝑜)‘𝑦))
wer 6219	wff 𝑅 Er 𝐴
cec 6220	class [𝐴]𝑅
cqs 6221	class (𝐴 / 𝑅)
df-er 6222	⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
df-ec 6224	⊢ [𝐴]𝑅 = (𝑅 “ {𝐴})
df-qs 6228	⊢ (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
cmap 6335	class ↑𝑚
cpm 6336	class ↑pm
df-map 6337	⊢ ↑𝑚 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥})
df-pm 6338	⊢ ↑pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓})
cen 6385	class ≈
cdom 6386	class ≼
cfn 6387	class Fin
df-en 6388	⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦}
df-dom 6389	⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦}
df-fin 6390	⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦}
csup 6584	class sup(𝐴, 𝐵, 𝑅)
cinf 6585	class inf(𝐴, 𝐵, 𝑅)
df-sup 6586	⊢ sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))}
df-inf 6587	⊢ inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)
cdju 6637	class (𝐴 ⊔ 𝐵)
df-dju 6638	⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1𝑜} × 𝐵))
cinl 6644	class inl
cinr 6645	class inr
df-inl 6646	⊢ inl = (𝑥 ∈ V ↦ ⟨∅, 𝑥⟩)
df-inr 6647	⊢ inr = (𝑥 ∈ V ↦ ⟨1𝑜, 𝑥⟩)
cdjucase 6681	class case(𝑅, 𝑆)
df-case 6682	⊢ case(𝑅, 𝑆) = ((𝑅 ∘ ◡inl) ∪ (𝑆 ∘ ◡inr))
cdjud 6689	class (𝑅 ⊔d 𝑆)
df-djud 6690	⊢ (𝑅 ⊔d 𝑆) = ((𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ◡(inr ↾ dom 𝑆)))
comni 6695	class Omni
df-omni 6696	⊢ Omni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2𝑜 → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1𝑜))}
ccrd 6710	class card
df-card 6711	⊢ card = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝑥})
cnpi 6734	class N
cpli 6735	class +N
cmi 6736	class ·N
clti 6737	class <N
cplpq 6738	class +pQ
cmpq 6739	class ·pQ
cltpq 6740	class <pQ
ceq 6741	class ~Q
cnq 6742	class Q
c1q 6743	class 1Q
cplq 6744	class +Q
cmq 6745	class ·Q
crq 6746	class *Q
cltq 6747	class <Q
ceq0 6748	class ~Q0
cnq0 6749	class Q0
c0q0 6750	class 0Q0
cplq0 6751	class +Q0
cmq0 6752	class ·Q0
cnp 6753	class P
c1p 6754	class 1P
cpp 6755	class +P
cmp 6756	class ·P
cltp 6757	class <P
cer 6758	class ~R
cnr 6759	class R
c0r 6760	class 0R
c1r 6761	class 1R
cm1r 6762	class -1R
cplr 6763	class +R
cmr 6764	class ·R
cltr 6765	class <R
df-ni 6766	⊢ N = (ω ∖ {∅})
df-pli 6767	⊢ +N = ( +𝑜 ↾ (N × N))
df-mi 6768	⊢ ·N = ( ·𝑜 ↾ (N × N))
df-lti 6769	⊢ <N = ( E ∩ (N × N))
df-plpq 6806	⊢ +pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨(((1st ‘𝑥) ·N (2nd ‘𝑦)) +N ((1st ‘𝑦) ·N (2nd ‘𝑥))), ((2nd ‘𝑥) ·N (2nd ‘𝑦))⟩)
df-mpq 6807	⊢ ·pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨((1st ‘𝑥) ·N (1st ‘𝑦)), ((2nd ‘𝑥) ·N (2nd ‘𝑦))⟩)
df-ltpq 6808	⊢ <pQ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ((1st ‘𝑥) ·N (2nd ‘𝑦)) <N ((1st ‘𝑦) ·N (2nd ‘𝑥)))}
df-enq 6809	⊢ ~Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))}
df-nqqs 6810	⊢ Q = ((N × N) / ~Q )
df-plqqs 6811	⊢ +Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ +pQ ⟨𝑢, 𝑓⟩)] ~Q ))}
df-mqqs 6812	⊢ ·Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)] ~Q ))}
df-1nqqs 6813	⊢ 1Q = [⟨1𝑜, 1𝑜⟩] ~Q
df-rq 6814	⊢ *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
df-ltnqqs 6815	⊢ <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
df-enq0 6886	⊢ ~Q0 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)))}
df-nq0 6887	⊢ Q0 = ((ω × N) / ~Q0 )
df-0nq0 6888	⊢ 0Q0 = [⟨∅, 1𝑜⟩] ~Q0
df-plq0 6889	⊢ +Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q0 ∧ 𝑦 ∈ Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·𝑜 𝑓) +𝑜 (𝑣 ·𝑜 𝑢)), (𝑣 ·𝑜 𝑓)⟩] ~Q0 ))}
df-mq0 6890	⊢ ·Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q0 ∧ 𝑦 ∈ Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨(𝑤 ·𝑜 𝑢), (𝑣 ·𝑜 𝑓)⟩] ~Q0 ))}
df-inp 6928	⊢ P = {⟨𝑙, 𝑢⟩ ∣ (((𝑙 ⊆ Q ∧ 𝑢 ⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ 𝑙 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑢)) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑢))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))))}
df-i1p 6929	⊢ 1P = ⟨{𝑙 ∣ 𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
df-iplp 6930	⊢ +P = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 +Q 𝑠))}⟩)
df-imp 6931	⊢ ·P = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1st ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (2nd ‘𝑦) ∧ 𝑞 = (𝑟 ·Q 𝑠))}⟩)
df-iltp 6932	⊢ <P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦)))}
df-enr 7175	⊢ ~R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (P × P) ∧ 𝑦 ∈ (P × P)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 +P 𝑢) = (𝑤 +P 𝑣)))}
df-nr 7176	⊢ R = ((P × P) / ~R )
df-plr 7177	⊢ +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R ))}
df-mr 7178	⊢ ·R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑓)), ((𝑤 ·P 𝑓) +P (𝑣 ·P 𝑢))⟩] ~R ))}
df-ltr 7179	⊢ <R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))}
df-0r 7180	⊢ 0R = [⟨1P, 1P⟩] ~R
df-1r 7181	⊢ 1R = [⟨(1P +P 1P), 1P⟩] ~R
df-m1r 7182	⊢ -1R = [⟨1P, (1P +P 1P)⟩] ~R
cc 7251	class ℂ
cr 7252	class ℝ
cc0 7253	class 0
c1 7254	class 1
ci 7255	class i
caddc 7256	class +
cltrr 7257	class <ℝ
cmul 7258	class ·
df-c 7259	⊢ ℂ = (R × R)
df-0 7260	⊢ 0 = ⟨0R, 0R⟩
df-1 7261	⊢ 1 = ⟨1R, 0R⟩
df-i 7262	⊢ i = ⟨0R, 1R⟩
df-r 7263	⊢ ℝ = (R × {0R})
df-add 7264	⊢ + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
df-mul 7265	⊢ · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}
df-lt 7266	⊢ <ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
ax-cnex 7339	⊢ ℂ ∈ V
ax-resscn 7340	⊢ ℝ ⊆ ℂ
ax-1cn 7341	⊢ 1 ∈ ℂ
ax-1re 7342	⊢ 1 ∈ ℝ
ax-icn 7343	⊢ i ∈ ℂ
ax-addcl 7344	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
ax-addrcl 7345	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
ax-mulcl 7346	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
ax-mulrcl 7347	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
ax-addcom 7348	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
ax-mulcom 7349	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
ax-addass 7350	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
ax-mulass 7351	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
ax-distr 7352	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
ax-i2m1 7353	⊢ ((i · i) + 1) = 0
ax-0lt1 7354	⊢ 0 <ℝ 1
ax-1rid 7355	⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
ax-0id 7356	⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
ax-rnegex 7357	⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
ax-precex 7358	⊢ ((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) → ∃𝑥 ∈ ℝ (0 <ℝ 𝑥 ∧ (𝐴 · 𝑥) = 1))
ax-cnre 7359	⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
ax-pre-ltirr 7360	⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <ℝ 𝐴)
ax-pre-ltwlin 7361	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵)))
ax-pre-lttrn 7362	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶))
ax-pre-apti 7363	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵)
ax-pre-ltadd 7364	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))
ax-pre-mulgt0 7365	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵)))
ax-pre-mulext 7366	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <ℝ (𝐵 · 𝐶) → (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)))
ax-arch 7367	⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛)
ax-caucvg 7368	⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    &   ⊢ (𝜑 → 𝐹:𝑁⟶ℝ)    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)))))
cpnf 7422	class +∞
cmnf 7423	class -∞
cxr 7424	class ℝ*
clt 7425	class <
cle 7426	class ≤
df-pnf 7427	⊢ +∞ = 𝒫 ∪ ℂ
df-mnf 7428	⊢ -∞ = 𝒫 +∞
df-xr 7429	⊢ ℝ* = (ℝ ∪ {+∞, -∞})
df-ltxr 7430	⊢ < = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
df-le 7431	⊢ ≤ = ((ℝ* × ℝ*) ∖ ◡ < )
cmin 7556	class −
cneg 7557	class -𝐴
df-sub 7558	⊢ − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
df-neg 7559	⊢ -𝐴 = (0 − 𝐴)
creap 7951	class #ℝ
df-reap 7952	⊢ #ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦 ∨ 𝑦 < 𝑥))}
cap 7958	class #
df-ap 7959	⊢ # = {⟨𝑥, 𝑦⟩ ∣ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ 𝑢))}
cdiv 8037	class /
df-div 8038	⊢ / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥))
cn 8316	class ℕ
df-inn 8317	⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
c2 8366	class 2
c3 8367	class 3
c4 8368	class 4
c5 8369	class 5
c6 8370	class 6
c7 8371	class 7
c8 8372	class 8
c9 8373	class 9
c10 8374	class 10
df-2 8375	⊢ 2 = (1 + 1)
df-3 8376	⊢ 3 = (2 + 1)
df-4 8377	⊢ 4 = (3 + 1)
df-5 8378	⊢ 5 = (4 + 1)
df-6 8379	⊢ 6 = (5 + 1)
df-7 8380	⊢ 7 = (6 + 1)
df-8 8381	⊢ 8 = (7 + 1)
df-9 8382	⊢ 9 = (8 + 1)
cn0 8565	class ℕ0
df-n0 8566	⊢ ℕ0 = (ℕ ∪ {0})
cxnn0 8628	class ℕ0*
xnninf 8629	class ℕ∞
df-xnn0 8630	⊢ ℕ0* = (ℕ0 ∪ {+∞})
df-nninf 8631	⊢ ℕ∞ = {𝑓 ∈ (2𝑜 ↑𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)}
cz 8646	class ℤ
df-z 8647	⊢ ℤ = {𝑛 ∈ ℝ ∣ (𝑛 = 0 ∨ 𝑛 ∈ ℕ ∨ -𝑛 ∈ ℕ)}
cdc 8772	class ;𝐴𝐵
df-dec 8773	⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
cuz 8914	class ℤ≥
df-uz 8915	⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘})
cq 8999	class ℚ
df-q 9000	⊢ ℚ = ( / “ (ℤ × ℕ))
crp 9029	class ℝ+
df-rp 9030	⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
cxne 9135	class -𝑒𝐴
cxad 9136	class +𝑒
cxmu 9137	class ·e
df-xneg 9138	⊢ -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
df-xadd 9139	⊢ +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))
df-xmul 9140	⊢ ·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
cioo 9201	class (,)
cioc 9202	class (,]
cico 9203	class [,)
cicc 9204	class [,]
df-ioo 9205	⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
df-ioc 9206	⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
df-ico 9207	⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
df-icc 9208	⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
cfz 9319	class ...
df-fz 9320	⊢ ... = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ (𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛)})
cfzo 9443	class ..^
df-fzo 9444	⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
cfl 9564	class ⌊
cceil 9565	class ⌈
df-fl 9566	⊢ ⌊ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℤ (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1))))
df-ceil 9567	⊢ ⌈ = (𝑥 ∈ ℝ ↦ -(⌊‘-𝑥))
cmo 9618	class mod
df-mod 9619	⊢ mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
cseq 9740	class seq𝑀( + , 𝐹, 𝑆)
df-iseq 9741	⊢ seq𝑀( + , 𝐹, 𝑆) = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
cexp 9791	class ↑
df-iexp 9792	⊢ ↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}), ℂ)‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}), ℂ)‘-𝑦)))))
cfa 9968	class !
df-fac 9969	⊢ ! = ({⟨0, 1⟩} ∪ seq1( · , I , ℂ))
cbc 9990	class C
df-bc 9991	⊢ C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
chash 10018	class ♯
df-ihash 10019	⊢ ♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}))
cshi 10076	class shift
df-shft 10077	⊢ shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)})
ccj 10100	class ∗
cre 10101	class ℜ
cim 10102	class ℑ
df-cj 10103	⊢ ∗ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ)))
df-re 10104	⊢ ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2))
df-im 10105	⊢ ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i)))
csqrt 10256	class √
cabs 10257	class abs
df-rsqrt 10258	⊢ √ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦)))
df-abs 10259	⊢ abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥))))
cli 10491	class ⇝
df-clim 10492	⊢ ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))}
csu 10564	class Σ𝑘 ∈ 𝐴 𝐵
df-isum 10565	⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)), ℂ)‘𝑚))))
cdvds 10576	class ∥
df-dvds 10577	⊢ ∥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)}
cgcd 10718	class gcd
df-gcd 10719	⊢ gcd = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦)}, ℝ, < )))
clcm 10822	class lcm
df-lcm 10823	⊢ lcm = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, inf({𝑛 ∈ ℕ ∣ (𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛)}, ℝ, < )))
cprime 10869	class ℙ
df-prm 10870	⊢ ℙ = {𝑝 ∈ ℕ ∣ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝} ≈ 2𝑜}
cnumer 10939	class numer
cdenom 10940	class denom
df-numer 10941	⊢ numer = (𝑦 ∈ ℚ ↦ (1st ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
df-denom 10942	⊢ denom = (𝑦 ∈ ℚ ↦ (2nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
cphi 10966	class ϕ
df-phi 10967	⊢ ϕ = (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}))
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wdcin 11036	wff 𝐴 DECIDin 𝐵
df-dcin 11037	⊢ (𝐴 DECIDin 𝐵 ↔ ∀𝑥 ∈ 𝐵 DECID 𝑥 ∈ 𝐴)
wbd 11046	wff BOUNDED 𝜑
ax-bd0 11047	⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (BOUNDED 𝜑 → BOUNDED 𝜓)
ax-bdim 11048	⊢ BOUNDED 𝜑    &   ⊢ BOUNDED 𝜓    ⇒   ⊢ BOUNDED (𝜑 → 𝜓)
ax-bdan 11049	⊢ BOUNDED 𝜑    &   ⊢ BOUNDED 𝜓    ⇒   ⊢ BOUNDED (𝜑 ∧ 𝜓)
ax-bdor 11050	⊢ BOUNDED 𝜑    &   ⊢ BOUNDED 𝜓    ⇒   ⊢ BOUNDED (𝜑 ∨ 𝜓)
ax-bdn 11051	⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED ¬ 𝜑
ax-bdal 11052	⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED ∀𝑥 ∈ 𝑦 𝜑
ax-bdex 11053	⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED ∃𝑥 ∈ 𝑦 𝜑
ax-bdeq 11054	⊢ BOUNDED 𝑥 = 𝑦
ax-bdel 11055	⊢ BOUNDED 𝑥 ∈ 𝑦
ax-bdsb 11056	⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED [𝑦 / 𝑥]𝜑
wbdc 11074	wff BOUNDED 𝐴
df-bdc 11075	⊢ (BOUNDED 𝐴 ↔ ∀𝑥BOUNDED 𝑥 ∈ 𝐴)
ax-bdsep 11118	⊢ BOUNDED 𝜑    ⇒   ⊢ ∀𝑎∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
ax-bj-d0cl 11158	⊢ BOUNDED 𝜑    ⇒   ⊢ DECID 𝜑
wind 11164	wff Ind 𝐴
df-bj-ind 11165	⊢ (Ind 𝐴 ↔ (∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))
ax-infvn 11179	⊢ ∃𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦))
ax-bdsetind 11206	⊢ BOUNDED 𝜑    ⇒   ⊢ (∀𝑎(∀𝑦 ∈ 𝑎 [𝑦 / 𝑎]𝜑 → 𝜑) → ∀𝑎𝜑)
ax-inf2 11214	⊢ ∃𝑎∀𝑥(𝑥 ∈ 𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦))
ax-strcoll 11220	⊢ ∀𝑎(∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑))
ax-sscoll 11225	⊢ ∀𝑎∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑))
ax-ddkcomp 11227	⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵)))
walsi 11230	wff ∀!𝑥(𝜑 → 𝜓)
walsc 11231	wff ∀!𝑥 ∈ 𝐴𝜑
df-alsi 11232	⊢ (∀!𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥𝜑))
df-alsc 11233	⊢ (∀!𝑥 ∈ 𝐴𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴))