axiom_of_power_set.test

<<< native
[ ESymbol Op "\8704"
, EIdentifier "A"
, ESpace (1 % 6)
, ESymbol Op "\8707"
, EIdentifier "P"
, ESpace (1 % 6)
, ESymbol Op "\8704"
, EIdentifier "B"
, ESpace (1 % 6)
, ESymbol Open "["
, EIdentifier "B"
, ESymbol Rel "\8712"
, EIdentifier "P"
, ESymbol Rel "\8660"
, ESymbol Op "\8704"
, EIdentifier "C"
, ESpace (1 % 6)
, ESymbol Open "("
, EIdentifier "C"
, ESymbol Rel "\8712"
, EIdentifier "B"
, ESymbol Rel "\8658"
, EIdentifier "C"
, ESymbol Rel "\8712"
, EIdentifier "A"
, ESymbol Close ")"
, ESymbol Close "]"
]
>>> starmath
forall A exists P forall B [B in P dlrarrow forall C (C in B drarrow C in A)]