Theorem dfss | index | src |

theorem dfss (A B: set) {x: nat}: $ A C_ B <-> A. x (x e. A -> x e. B) $;
StepHypRefExpression
1 biid
A C_ B <-> A C_ B
2 1 conv subset
A C_ B <-> A. x (x e. A -> x e. B)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)