Theorem sabfin ≪ | index | src | ≫

theorem sabfin (A: set) (G: wff) {x y: nat} (B: set x):
  $ G -> y e. B -> x e. A $ >
  $ G -> finite A $ >
  $ G /\ x e. A -> finite B $ >
  $ G -> finite (S\ x, B) $;

G -> y e. B -> x e. A

G -> S\ x, B == X\ x e. A, B

G -> (finite (S\ x, B) <-> finite (X\ x e. A, B))

G -> finite A

G /\ x e. A -> finite B

G -> finite (X\ x e. A, B)

G -> finite (S\ x, B)

Axiom use