Step |
Hyp |
Ref |
Expression |
1 |
|
bnj124.1 |
|
2 |
|
bnj124.2 |
Could not format ( ph" <-> [. F / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. F / f ]. ph' ) with typecode |- |
3 |
|
bnj124.3 |
Could not format ( ps" <-> [. F / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |- |
4 |
|
bnj124.4 |
Could not format ( ze" <-> [. F / f ]. ze' ) : No typesetting found for |- ( ze" <-> [. F / f ]. ze' ) with typecode |- |
5 |
|
bnj124.5 |
Could not format ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |- |
6 |
5
|
sbcbii |
Could not format ( [. F / f ]. ze' <-> [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( [. F / f ]. ze' <-> [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |- |
7 |
1
|
bnj95 |
|
8 |
|
nfv |
|
9 |
8
|
sbc19.21g |
Could not format ( F e. _V -> ( [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) ) ) : No typesetting found for |- ( F e. _V -> ( [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) ) ) with typecode |- |
10 |
7 9
|
ax-mp |
Could not format ( [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( [. F / f ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |- |
11 |
|
fneq1 |
|
12 |
|
fneq1 |
|
13 |
11 12
|
sbcie2g |
|
14 |
7 13
|
ax-mp |
|
15 |
14
|
bicomi |
|
16 |
15 2 3 7
|
bnj206 |
Could not format ( [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) <-> ( F Fn 1o /\ ph" /\ ps" ) ) : No typesetting found for |- ( [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) <-> ( F Fn 1o /\ ph" /\ ps" ) ) with typecode |- |
17 |
16
|
imbi2i |
Could not format ( ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) -> [. F / f ]. ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) with typecode |- |
18 |
6 10 17
|
3bitri |
Could not format ( [. F / f ]. ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) : No typesetting found for |- ( [. F / f ]. ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) with typecode |- |
19 |
4 18
|
bitri |
Could not format ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) : No typesetting found for |- ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) with typecode |- |