Theorem hbss 2065

Description: If x is not free in A and B, it is not free in A (_ B.

Hypotheses

Ref	Expression
dfss2f.1	|- (y e. A -> A.x y e. A)
dfss2f.2	|- (y e. B -> A.x y e. B)

Assertion

Ref	Expression
hbss	|- (A (_ B -> A.x A (_ B)

Distinct variable groups:   y,A   y,B   x,y

Proof of Theorem hbss

Step	Hyp	Ref	Expression
1		hba1 1005	. 2 |- (A.x(x e. A -> x e. B) -> A.xA.x(x e. A -> x e. B))
2		dfss2f.1	. . 3 |- (y e. A -> A.x y e. A)
3		dfss2f.2	. . 3 |- (y e. B -> A.x y e. B)
4	2, 3	dfss2f 2063	. 2 |- (A (_ B <-> A.x(x e. A -> x e. B))
5	4	albii 1001	. 2 |- (A.x A (_ B <-> A.xA.x(x e. A -> x e. B))
6	1, 4, 5	3imtr4 219	1 |- (A (_ B -> A.x A (_ B)

Syntax hints:   -> wi 3  A.wal 956   e. wcel 960   (_ wss 2050

This theorem is referenced by:  hbpw 2411  ssiun2s 2598  ssopab2 2828  hbrel 3251  hbfun 3542  hbf 3631  rnssopab 3831  fopabco 3838  oawordeulem 4194  r1val1 4668  cardaleph 4896  tgval3t 7624  fgsb 10555  fgsb2 10560

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056

Copyright terms: Public domain