theorem xabeq2da (A: set) (G: wff) {x: nat} (B C: set x):
$ G /\ x e. A -> B == C $ >
$ G -> X\ x e. A, B == X\ x e. A, C $;
Step | Hyp | Ref | Expression |
1 |
|
aneq2a |
(fst z e. A -> (snd z e. S[fst z / x] B <-> snd z e. S[fst z / x] C)) -> (fst z e. A /\ snd z e. S[fst z / x] B <-> fst z e. A /\ snd z e. S[fst z / x] C) |
2 |
|
eleq2 |
S[fst z / x] B == S[fst z / x] C -> (snd z e. S[fst z / x] B <-> snd z e. S[fst z / x] C) |
3 |
|
nfv |
F/ x fst z e. A |
4 |
|
nfsbs1 |
FS/ x S[fst z / x] B |
5 |
|
nfsbs1 |
FS/ x S[fst z / x] C |
6 |
4, 5 |
nfeqs |
F/ x S[fst z / x] B == S[fst z / x] C |
7 |
3, 6 |
nfim |
F/ x fst z e. A -> S[fst z / x] B == S[fst z / x] C |
8 |
|
eleq1 |
x = fst z -> (x e. A <-> fst z e. A) |
9 |
|
sbsq |
x = fst z -> B == S[fst z / x] B |
10 |
|
sbsq |
x = fst z -> C == S[fst z / x] C |
11 |
9, 10 |
eqseqd |
x = fst z -> (B == C <-> S[fst z / x] B == S[fst z / x] C) |
12 |
8, 11 |
imeqd |
x = fst z -> (x e. A -> B == C <-> fst z e. A -> S[fst z / x] B == S[fst z / x] C) |
13 |
7, 12 |
ealeh |
A. x (x e. A -> B == C) -> fst z e. A -> S[fst z / x] B == S[fst z / x] C |
14 |
|
hyp h |
G /\ x e. A -> B == C |
15 |
14 |
ialda |
G -> A. x (x e. A -> B == C) |
16 |
13, 15 |
syl |
G -> fst z e. A -> S[fst z / x] B == S[fst z / x] C |
17 |
2, 16 |
syl6 |
G -> fst z e. A -> (snd z e. S[fst z / x] B <-> snd z e. S[fst z / x] C) |
18 |
1, 17 |
syl |
G -> (fst z e. A /\ snd z e. S[fst z / x] B <-> fst z e. A /\ snd z e. S[fst z / x] C) |
19 |
18 |
abeqd |
G -> {z | fst z e. A /\ snd z e. S[fst z / x] B} == {z | fst z e. A /\ snd z e. S[fst z / x] C} |
20 |
19 |
conv xab |
G -> X\ x e. A, B == X\ x e. A, C |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp,
itru),
axs_pred_calc
(ax_gen,
ax_4,
ax_5,
ax_6,
ax_7,
ax_10,
ax_11,
ax_12),
axs_set
(elab,
ax_8)